Theorems · Theorem · number theory
Nat.totient_prime_pow
∀ {p : ℕ}, Nat.Prime p → ∀ {n : ℕ}, 0 < n → (p ^ n).totient = p ^ (n - 1) * (p - 1)When p is prime, then the totient of p ^ n is p ^ (n - 1) * (p - 1)
- Defined in
- Mathlib.Data.Nat.Totient
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.Primestatement and proof · cited by 2,059
- pos_iff_ne_zeroproof · cited by 180
- Nat.totientstatement · cited by 111
- Nat.totient_prime_pow_succproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- Nat.totient_primeproof · cited by 11
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- IsPrimitiveRoot.norm_pow_sub_one_twoproof · cited by 3
- IsCyclic.normalizer_le_centralizerproof · cited by 2
- Nat.totient_eq_prod_factorizationproof · cited by 2
- IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_twoproof · cited by 1
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1
- IsCyclotomicExtension.Rat.discr_prime_pow_succproof · cited by 1
- Nat.prime_pow_pow_totient_ediv_prodproof · cited by 1
- ArithmeticFunction.carmichael_two_pow_of_ne_twoproof · cited by 1
- ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totientproof · cited by 0