Theorems · Theorem · number theory
Polynomial.prod_cyclotomic_eq_X_pow_sub_one
∀ {n : ℕ},
0 < n → ∀ (R : Type u_1) [inst : CommRing R], ∏ i ∈ n.divisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Polynomialstatement · cited by 5,681
- Complexproof · cited by 5,565
- Finset.prodstatement and proof · cited by 2,356
- Polynomial.Xstatement and proof · cited by 1,639
- LT.lt.ne'proof · cited by 1,417
- Polynomial.mapproof · cited by 806
- Finset.prod_congrproof · cited by 646
- Int.castRingHomproof · cited by 254
- Nat.divisorsstatement and proof · cited by 137
- Polynomial.cyclotomicstatement and proof · cited by 130
- Polynomial.map_Xproof · cited by 122
Cited by11
Results whose statement or proof uses this declaration.
- Polynomial.prod_cyclotomic_eq_geom_sumproof · cited by 4
- isRoot_of_unity_iffproof · cited by 3
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- Polynomial.cyclotomic_eq_X_pow_sub_one_divproof · cited by 2
- Polynomial.eq_cyclotomic_iffproof · cited by 2
- Polynomial.cyclotomic.dvd_X_pow_sub_oneproof · cited by 2
- Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvdproof · cited by 1
- Polynomial.isRoot_of_unity_of_root_cyclotomicproof · cited by 0
- Polynomial.orderOf_root_cyclotomic_dvdproof · cited by 0
- Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebiusproof · cited by 0
- Polynomial.X_pow_sub_one_dvd_prod_cyclotomicproof · cited by 0