Theorems · Theorem · number theory
IsPrimitiveRoot.pow_of_coprime
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
IsPrimitiveRoot ζ k → ∀ (i : ℕ), i.Coprime k → IsPrimitiveRoot (ζ ^ i) k- Cited by
- 8 results in Mathlib
- Foundations
- Depth 38 from the axioms · uses propext, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- Unitsproof · cited by 2,804
- CommMonoidstatement and proof · cited by 2,264
- Units.valproof · cited by 1,966
- pow_oneproof · cited by 894
- one_powproof · cited by 521
- IsPrimitiveRootstatement and proof · cited by 356
- zpow_natCastproof · cited by 271
- mul_powproof · cited by 220
- pow_mulproof · cited by 210
- mul_right_commproof · cited by 108
- IsPrimitiveRoot.pow_eq_oneproof · cited by 48
Cited by8
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.card_primitiveRootsproof · cited by 4
- IsPrimitiveRoot.pow_iff_coprimeproof · cited by 3
- IsPrimitiveRoot.isPrimitiveRoot_iffproof · cited by 3
- IsPrimitiveRoot.pow_of_primeproof · cited by 2
- IsPrimitiveRoot.minpoly_eq_pow_coprimeproof · cited by 1
- IsPrimitiveRoot.zpow_of_gcd_eq_oneproof · cited by 0
- IsPrimitiveRoot.isPrimitiveRoot_iff'proof · cited by 0
- IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruentproof · cited by 0