PowModTotient

Statistics

Metric	Count
Definitions	0
Theorems `pow_add_mul_totient_mod_eq`, `pow_add_totient_mod_eq`, `pow_totient_mod`, `pow_totient_mod_eq_one`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_add_mul_totient_mod_eq` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `totient`	—	`MulZeroClass.zero_mul` `add_zero` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_assoc` `pow_add_totient_mod_eq`
`pow_add_totient_mod_eq` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `totient`	—	`pow_add` `pow_totient_mod_eq_one` `mul_one`
`pow_totient_mod` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `totient`	—	`add_comm` `pow_add_mul_totient_mod_eq`
`pow_totient_mod_eq_one` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `totient`	—	`mod_eq_of_modEq` `ModEq.pow_totient`

---