Theorems · Theorem · number theory
IsPrimitiveRoot.eq_pow_of_pow_eq_one
∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ ξ : R},
IsPrimitiveRoot ζ k → ξ ^ k = 1 → ∃ i < k, ζ ^ i = ξ- Cited by
- 17 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Unitsproof · cited by 2,804
- IsDomainstatement and proof · cited by 2,196
- Units.valproof · cited by 1,966
- IsPrimitiveRootstatement and proof · cited by 356
- IsPrimitiveRoot.isUnitproof · cited by 22
- IsPrimitiveRoot.coe_units_iffproof · cited by 11
- IsUnit.of_pow_eq_oneproof · cited by 4
- mem_rootsOfUnity'proof · cited by 3
- IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnityproof · cited by 3
Cited by17
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.isPrimitiveRoot_iffproof · cited by 3
- isCyclotomicExtension_singleton_iff_eq_adjoinproof · cited by 3
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_rootsproof · cited by 3
- IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_primeproof · cited by 2
- IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eqproof · cited by 2
- MulChar.apply_mem_algebraAdjoin_of_pow_eq_oneproof · cited by 2
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomicproof · cited by 2
- Complex.mem_rootsOfUnityproof · cited by 1
- IsPrimitiveRoot.adjoin_pair_eqproof · cited by 1
- Complex.isPrimitiveRoot_iffproof · cited by 1
- IsCyclotomicExtension.isMulCommutativeproof · cited by 1
- IsCyclotomicExtension.mem_of_pow_eq_oneproof · cited by 1