Theorems · Definition · number theory
IsPrimitiveRoot.toInteger
{K : Type u} → [inst : Field K] → {ζ : K} → {k : ℕ} → [NeZero k] → IsPrimitiveRoot ζ k → NumberField.RingOfIntegers KAbbreviation to see a primitive root of unity as a member of the ring of integers.
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
Cited by72
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.toInteger_isPrimitiveRootstatement · cited by 15
- IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_twostatement and proof · cited by 5
- IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_onestatement and proof · cited by 4
- IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_onestatement and proof · cited by 4
- IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOverstatement and proof · cited by 3
- IsPrimitiveRoot.integralPowerBasisOfPrimePow_genstatement and proof · cited by 3
- IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_twostatement and proof · cited by 3
- IsCyclotomicExtension.Rat.adjoin_singleton_eq_topstatement and proof · cited by 3
- IsCyclotomicExtension.Rat.associated_norm_zeta_sub_onestatement · cited by 3
- IsCyclotomicExtension.Rat.discr_prime_powproof · cited by 2
- IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'statement · cited by 2
- IsPrimitiveRoot.zeta_sub_one_primestatement · cited by 2