Theorems · Theorem · number theory
Nat.totient_prime_pow_succ
∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℕ), (p ^ (n + 1)).totient = p ^ n * (p - 1)When p is prime, then the totient of p ^ (n + 1) is p ^ n * (p - 1)
- Defined in
- Mathlib.Data.Nat.Totient
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- one_mulproof · cited by 2,841
- Finset.cardproof · cited by 2,327
- mul_commproof · cited by 2,262
- Nat.Primestatement and proof · cited by 2,059
- Finset.rangeproof · cited by 1,341
- Finset.filterproof · cited by 949
- Finset.imageproof · cited by 910
- Finset.filter_congrproof · cited by 167
- Nat.totientstatement · cited by 111
- Nat.Prime.ne_zeroproof · cited by 109
- Finset.card_rangeproof · cited by 108
Cited by4
Results whose statement or proof uses this declaration.
- Nat.totient_prime_powproof · cited by 13
- IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_oneproof · cited by 4
- ZMod.isCyclic_units_of_prime_powproof · cited by 2
- IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_powproof · cited by 2