Theorems · Theorem · number theory
IsPrimitiveRoot.idealQuotient_mk
∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} [inst_1 : NumberField K] {n : ℕ} [NeZero n]
{ζ : NumberField.RingOfIntegers K},
IsPrimitiveRoot ζ n → Ideal.absNorm I ≠ 1 → (Ideal.absNorm I).Coprime n → IsPrimitiveRoot ((Ideal.Quotient.mk I) ζ) n- Cited by
- 1 results in Mathlib
- Foundations
- Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldNumberFieldNeZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHomstatement · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Idealstatement and proof · cited by 4,748
- HasQuotient.Quotientstatement · cited by 2,301
- MonoidWithZeroHomstatement · cited by 704
- NumberFieldstatement and proof · cited by 653
- Ideal.Quotient.mkstatement · cited by 610
- NumberField.RingOfIntegersstatement and proof · cited by 413
- IsPrimitiveRootstatement and proof · cited by 356
- Ideal.absNormstatement and proof · cited by 123
- IsPrimitiveRoot.map_of_injectiveproof · cited by 19
Cited by1
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizerproof · cited by 1