Theorems · Theorem · number theory
Polynomial.cyclotomic_eq_minpoly
∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K},
IsPrimitiveRoot μ n → 0 < n → ∀ [CharZero K], Polynomial.cyclotomic n ℤ = minpoly ℤ μcyclotomic n ℤ is the minimal polynomial of a primitive n-th root of unity μ.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Polynomialstatement · cited by 5,681
- Polynomial.natDegreeproof · cited by 1,105
- CharZerostatement and proof · cited by 932
- minpolystatement and proof · cited by 439
- IsPrimitiveRootstatement and proof · cited by 356
- Polynomial.cyclotomicstatement · cited by 130
- minpoly.monicproof · cited by 81
- IsPrimitiveRoot.isIntegralproof · cited by 15
- Polynomial.natDegree_cyclotomicproof · cited by 12
- Polynomial.cyclotomic.monicproof · cited by 12
- Polynomial.eq_of_monic_of_dvd_of_natDegree_leproof · cited by 7
Cited by7
Results whose statement or proof uses this declaration.
- Polynomial.cyclotomic_eq_minpoly_ratproof · cited by 2
- Polynomial.cyclotomic_expand_eq_cyclotomicproof · cited by 2
- Polynomial.cyclotomic.irreducibleproof · cited by 1
- IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvdproof · cited by 1
- IsPrimitiveRoot.integralPowerBasisOfPrimePow_dimproof · cited by 1
- IsPrimitiveRoot.integralPowerBasis_dimproof · cited by 0
- Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_oneproof · cited by 0