Theorems · Theorem · number theory
IsPrimitiveRoot.pow
∀ {M : Type u_1} [inst : CommMonoid M] {ζ : M} {n a b : ℕ},
0 < n → IsPrimitiveRoot ζ n → n = a * b → IsPrimitiveRoot (ζ ^ a) bIf there is an n-th primitive root of unity in R and b divides n,
then there is a b-th primitive root of unity in R.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- CommMonoid
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.
- CommMonoidstatement and proof · cited by 2,264
- IsPrimitiveRootstatement and proof · cited by 356
- IsPrimitiveRoot.pow_eq_oneproof · cited by 48
- IsPrimitiveRoot.dvd_of_pow_eq_oneproof · cited by 12
Cited by8
Results whose statement or proof uses this declaration.
- Polynomial.cyclotomic_eq_prod_X_sub_primitiveRootsproof · cited by 5
- HasEnoughRootsOfUnity.of_dvdproof · cited by 5
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- IsCyclotomicExtension.Rat.adjoin_singleton_eq_topproof · cited by 3
- Polynomial.int_coeff_of_cyclotomic'proof · cited by 3
- modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_powproof · cited by 2
- IsCyclotomicExtension.Rat.discrproof · cited by 1
- IsCyclotomicExtension.le_of_dvdproof · cited by 1