Theorems · Theorem · number theory
IsPrimitiveRoot.toInteger_isPrimitiveRoot
∀ {K : Type u} [inst : Field K] {ζ : K} {k : ℕ} [inst_1 : NeZero k] (hζ : IsPrimitiveRoot ζ k),
IsPrimitiveRoot hζ.toInteger k- Cited by
- 15 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- NumberField.RingOfIntegersstatement · cited by 413
- IsPrimitiveRootstatement and proof · cited by 356
- IsPrimitiveRoot.toIntegerstatement · cited by 72
- NumberField.RingOfIntegers.coe_injectiveproof · cited by 9
- IsPrimitiveRoot.of_map_of_injectiveproof · cited by 2
Cited by15
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.associated_sub_one_of_isPrimitiveRootproof · cited by 1
- IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_primeproof · cited by 1
- IsCyclotomicExtension.Rat.Three.Units.memstatement and proof · cited by 1
- IsPrimitiveRoot.toInteger_cube_eq_oneproof · cited by 1
- IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mulstatement and proof · cited by 1
- IsCyclotomicExtension.Rat.Three.eta_sqstatement and proof · cited by 1
- IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_onestatement and proof · cited by 1
- IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_onestatement and proof · cited by 1
- NumberField.Units.dvd_torsionOrder_of_isPrimitiveRootproof · cited by 1
- IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_powproof · cited by 1
- IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizerproof · cited by 1