Theorems · Theorem · number theory
IsPrimitiveRoot.eq_orderOf
∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → k = orderOf ζ- Cited by
- 18 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- orderOfstatement · cited by 324
- IsPrimitiveRoot.orderOfproof · cited by 10
- IsPrimitiveRoot.uniqueproof · cited by 8
Cited by18
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.map_of_injectiveproof · cited by 19
- HasEnoughRootsOfUnity.natCard_rootsOfUnityproof · cited by 5
- IsPrimitiveRoot.autToPow_specproof · cited by 5
- IsPrimitiveRoot.pow_mul_pow_lcmproof · cited by 4
- IsPrimitiveRoot.pow_of_dvdproof · cited by 4
- IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprimeproof · cited by 3
- NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_ltproof · cited by 2
- IsPrimitiveRoot.of_map_of_injectiveproof · cited by 2
- IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_applyproof · cited by 1
- Nat.exists_prime_gt_modEq_oneproof · cited by 1
- Polynomial.cyclotomic_injectiveproof · cited by 1
- IsCyclic.exists_apply_ne_oneproof · cited by 1