Basic

📁 Source: Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Statistics

Metric	Count
Definitions `cyclotomic`, `cyclotomic'`	2
Theorems `pow_add_pow_eq_prod_add_mul`, `pow_sub_pow_eq_prod_sub_mul`, `X_pow_sub_one_dvd_prod_cyclotomic`, `X_pow_sub_one_eq_prod`, `X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd`, `X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd`, `X_pow_sub_one_splits`, `coprime_of_root_cyclotomic`, `monic`, `cyclotomic'_eq_X_pow_sub_one_div`, `cyclotomic'_ne_zero`, `cyclotomic'_one`, `cyclotomic'_splits`, `cyclotomic'_two`, `cyclotomic'_zero`, `dvd_X_pow_sub_one`, `eval_apply`, `eval_apply_ofReal`, `isPrimitive`, `monic`, `cyclotomic_coeff_zero`, `cyclotomic_dvd_geom_sum_of_dvd`, `cyclotomic_eq_X_pow_sub_one_div`, `cyclotomic_eq_prod_X_pow_sub_one_pow_moebius`, `cyclotomic_eq_prod_X_sub_primitiveRoots`, `cyclotomic_ne_zero`, `cyclotomic_one`, `cyclotomic_prime`, `cyclotomic_prime_mul_X_sub_one`, `cyclotomic_prime_pow_eq_geom_sum`, `cyclotomic_prime_pow_mul_X_pow_sub_one`, `cyclotomic_three`, `cyclotomic_two`, `cyclotomic_zero`, `degree_cyclotomic`, `degree_cyclotomic'`, `degree_cyclotomic_pos`, `dvd_C_mul_X_sub_one_pow_add_one`, `eq_cyclotomic_iff`, `int_coeff_of_cyclotomic'`, `int_cyclotomic_rw`, `int_cyclotomic_spec`, `int_cyclotomic_unique`, `map_cyclotomic`, `map_cyclotomic_int`, `natDegree_cyclotomic`, `natDegree_cyclotomic'`, `natDegree_cyclotomic_le`, `orderOf_root_cyclotomic_dvd`, `prod_cyclotomic'_eq_X_pow_sub_one`, `prod_cyclotomic_eq_X_pow_sub_one`, `prod_cyclotomic_eq_geom_sum`, `roots_of_cyclotomic`, `separable_cyclotomic`, `squarefree_cyclotomic`, `unique_int_coeff_of_cycl`	56
Total	58

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_add_pow_eq_prod_add_mul` 📖	mathematical	`Odd` `Nat.instSemiring` `IsPrimitiveRoot` `CommRing.toCommMonoid`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset.prod` `Polynomial.nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul`	—	`Odd.neg_pow` `sub_neg_eq_add` `Finset.prod_congr` `mul_neg` `pow_sub_pow_eq_prod_sub_mul` `Odd.pos` `Nat.instCanonicallyOrderedAdd` `Nat.instNontrivial`
`pow_sub_pow_eq_prod_sub_mul` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset.prod` `Polynomial.nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`FaithfulSMul.algebraMap_injective` `FractionRing.instFaithfulSMul` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsDomain.toNontrivial` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_prod` `Finset.prod_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_of_injective` `instIsDomain` `Finset.prod_nbij` `Polynomial.map_mem_nthRootsFinset_one` `Set.surj_on_of_inj_on_of_ncard_le` `Set.ncard_coe_finset` `card_nthRootsFinset` `Set.toFinite` `Finite.of_fintype`

Polynomial

Definitions

Name	Category	Theorems
`cyclotomic` 📖	CompOp	82 math math: `eval₂_one_cyclotomic_prime`, `eq_cyclotomic_iff`, `cyclotomic_six`, `cyclotomic.irreducible`, `cyclotomic_dvd_geom_sum_of_dvd`, `cyclotomic_pos'`, `sub_one_pow_totient_le_cyclotomic_eval`, `cyclotomic_expand_eq_cyclotomic_mul`, `IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic`, `cyclotomic.eval_apply_ofReal`, `IsCyclotomicExtension.aeval_zeta`, `prod_cyclotomic_eq_X_pow_sub_one`, `cyclotomic_eval_lt_add_one_pow_totient`, `natDegree_cyclotomic`, `cyclotomic_two`, `squarefree_cyclotomic`, `X_pow_sub_one_dvd_prod_cyclotomic`, `sub_one_pow_totient_lt_natAbs_cyclotomic_eval`, `sub_one_lt_natAbs_cyclotomic_eval`, `cyclotomic_eq_prod_X_sub_primitiveRoots`, `cyclotomic.roots_to_finset_eq_primitiveRoots`, `int_cyclotomic_rw`, `cyclotomic_mul_prime_dvd_eq_pow`, `IsCyclotomicExtension.splits_cyclotomic`, `roots_cyclotomic_nodup`, `isRoot_cyclotomic_iff_charZero`, `cyclotomic_prime_pow_eq_geom_sum`, `cyclotomic_pos_and_nonneg`, `cyclotomic.isCoprime_rat`, `cyclotomic_prime_pow_mul_X_pow_sub_one`, `eval_one_cyclotomic_prime_pow`, `cyclotomic_coeff_zero`, `cyclotomic_zero`, `cyclotomic.dvd_X_pow_sub_one`, `cyclotomic_dvd_of_mahlerMeasure_eq_one`, `cyclotomic.isPrimitive`, `cyclotomic_injective`, `IsCyclotomicExtension.zeta_isRoot`, `cyclotomic.roots_eq_primitiveRoots_val`, `cyclotomic_mul_prime_pow_eq`, `cyclotomic.eval_apply`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `natDegree_cyclotomic_le`, `X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd`, `eval_one_cyclotomic_not_prime_pow`, `eval_one_cyclotomic_prime`, `cyclotomic.monic`, `cyclotomic_eq_minpoly_rat`, `cyclotomic_mul_prime_eq_pow_of_not_dvd`, `cyclotomic_one`, `prod_cyclotomic_eq_geom_sum`, `map_cyclotomic_int`, `cyclotomic_eq_prod_X_pow_sub_one_pow_moebius`, `cyclotomic_nonneg`, `cyclotomic.irreducible_rat`, `IsCyclotomicExtension.splitting_field_cyclotomic`, `map_cyclotomic`, `cyclotomic_eval_le_add_one_pow_totient`, `cyclotomic_three`, `cyclotomic_comp_X_add_one_isEisensteinAt`, `separable_cyclotomic`, `eval₂_one_cyclotomic_prime_pow`, `isRoot_cyclotomic_prime_pow_mul_iff_of_charP`, `sub_one_pow_totient_lt_cyclotomic_eval`, `cyclotomic_prime`, `degree_cyclotomic_pos`, `cyclotomic_mahlerMeasure_eq_one`, `cyclotomic_expand_eq_cyclotomic`, `IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots`, `X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd`, `IsPrimitiveRoot.minpoly_dvd_cyclotomic`, `cyclotomic_eq_minpoly`, `isRoot_of_unity_iff`, `cyclotomic_eq_X_pow_sub_one_div`, `degree_cyclotomic`, `cyclotomic_prime_mul_X_sub_one`, `cyclotomic_pos`, `normalizedFactors_cyclotomic_card`, `isRoot_cyclotomic_iff`, `int_cyclotomic_unique`, `IsPrimitiveRoot.isRoot_cyclotomic`, `int_cyclotomic_spec`
`cyclotomic'` 📖	CompOp	14 math math: `int_coeff_of_cyclotomic'`, `unique_int_coeff_of_cycl`, `cyclotomic'.monic`, `cyclotomic'_one`, `int_cyclotomic_rw`, `prod_cyclotomic'_eq_X_pow_sub_one`, `cyclotomic'_two`, `roots_of_cyclotomic`, `degree_cyclotomic'`, `cyclotomic'_splits`, `natDegree_cyclotomic'`, `cyclotomic'_zero`, `cyclotomic'_eq_X_pow_sub_one_div`, `int_cyclotomic_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_pow_sub_one_dvd_prod_cyclotomic` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `CommRing.toRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `Finset.prod` `CommRing.toCommMonoid` `Nat.properDivisors` `cyclotomic`	—	`Nat.mem_properDivisors` `lt_of_le_of_ne` `Nat.divisor_le` `Nat.mem_divisors` `LT.lt.ne'` `Finset.sdiff_union_of_subset` `Nat.divisors_subset_properDivisors` `ne_of_lt` `Finset.prod_union` `Finset.sdiff_disjoint` `prod_cyclotomic_eq_X_pow_sub_one` `Nat.pos_of_mem_properDivisors` `mul_comm`
`X_pow_sub_one_eq_prod` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSub` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `Finset.prod` `commRing` `nthRootsFinset` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`nthRootsFinset.eq_1` `IsPrimitiveRoot.nthRoots_one_nodup` `Multiset.toFinset_eq` `nthRoots.eq_1` `monic_X_pow_sub_C` `ne_of_lt` `prod_multiset_X_sub_C_of_monic_of_roots_card_eq` `natDegree_X_pow_sub_C` `IsDomain.toNontrivial` `IsPrimitiveRoot.card_nthRoots_one`
`X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd` 📖	mathematical	`Finset` `Finset.instMembership` `Nat.properDivisors`	`Polynomial` `Ring.toSemiring` `CommRing.toRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `instMul` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `cyclotomic`	—	`X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd` `Nat.mem_properDivisors` `LT.lt.ne_bot` `Nat.insert_self_properDivisors` `Finset.insert_sdiff_of_notMem` `LT.lt.not_ge` `Nat.divisor_le` `Finset.prod_insert` `Finset.notMem_sdiff_of_notMem_left` `Nat.self_notMem_properDivisors` `mul_assoc`
`X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `CommRing.toRing` `instMul` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Finset` `Finset.instSDiff` `Nat.divisors` `cyclotomic`	—	`lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `prod_cyclotomic_eq_X_pow_sub_one` `mul_comm` `Finset.prod_sdiff` `Nat.divisors_subset_of_dvd` `ne_of_gt`
`X_pow_sub_one_splits` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`instIsDomain` `splits_iff_card_roots` `nthRoots.eq_1` `IsPrimitiveRoot.card_nthRoots_one` `natDegree_X_pow_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`coprime_of_root_cyclotomic` 📖	—	`IsRoot` `ZMod` `Ring.toSemiring` `CommRing.toRing` `ZMod.commRing` `cyclotomic` `DFunLike.coe` `RingHom` `Nat.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Nat.castRingHom`	—	—	`Nat.Prime.coprime_iff_not_dvd` `Fact.out` `ZMod.natCast_eq_zero_iff` `cyclotomic_one` `coeff_sub` `coeff_X_zero` `coeff_one_zero` `zero_sub` `NeZero.one` `ZMod.nontrivial` `Nat.Prime.one_lt'` `coeff_zero_eq_eval_zero` `eq_natCast` `RingHom.instRingHomClass` `IsRoot.def` `one_ne_zero` `cyclotomic_coeff_zero` `lt_of_le_of_ne`
`cyclotomic'_eq_X_pow_sub_one_div` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`cyclotomic'` `divByMonic` `CommRing.toRing` `Polynomial` `Ring.toSemiring` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `Finset.prod` `commRing` `Nat.properDivisors`	—	`prod_cyclotomic'_eq_X_pow_sub_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne'` `Finset.prod_cons` `monic_prod_of_monic` `cyclotomic'.monic` `div_modByMonic_unique` `zero_add` `mul_comm` `bot_lt_iff_ne_bot` `Monic.ne_zero` `IsDomain.toNontrivial` `degree_eq_bot`
`cyclotomic'_ne_zero` 📖	—	—	—	—	`Monic.ne_zero` `IsDomain.toNontrivial` `cyclotomic'.monic`
`cyclotomic'_one` 📖	mathematical	—	`cyclotomic'` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSub` `CommRing.toRing` `X` `instOne`	—	`Finset.prod_congr` `IsPrimitiveRoot.primitiveRoots_one` `Finset.prod_singleton` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`cyclotomic'_splits` 📖	mathematical	—	`Splits` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `cyclotomic'` `instIsDomain` `Field.toSemifield`	—	`Splits.prod` `instIsDomain`
`cyclotomic'_two` 📖	mathematical	—	`cyclotomic'` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instAdd` `X` `instOne`	—	`cyclotomic'.eq_1` `Nat.instAtLeastTwoHAddOfNat` `mem_primitiveRoots` `two_pos` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsPrimitiveRoot.neg_one` `IsDomain.toNontrivial` `IsPrimitiveRoot.eq_neg_one_of_two_right` `IsDomain.to_noZeroDivisors` `Finset.prod_congr` `Finset.prod_singleton` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `sub_neg_eq_add`
`cyclotomic'_zero` 📖	mathematical	—	`cyclotomic'` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOne`	—	`Finset.prod_congr` `primitiveRoots_zero`
`cyclotomic_coeff_zero` 📖	mathematical	—	`coeff` `Ring.toSemiring` `CommRing.toRing` `cyclotomic` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Nat.strong_induction_on` `Finset.insert_erase` `Nat.one_mem_properDivisors_iff_one_lt` `lt_of_lt_of_le` `Nat.instAtLeastTwoHAddOfNat` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.prod_insert` `Finset.notMem_erase` `cyclotomic_one` `Ne.le_iff_lt` `Finset.mem_erase` `Nat.pos_of_mem_properDivisors` `Nat.mem_properDivisors` `Finset.prod_congr` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv` `Finset.prod_const_one` `coeff_sub` `coeff_X_zero` `coeff_one_zero` `zero_sub` `mul_one` `prod_cyclotomic_eq_X_pow_sub_one` `LE.le.trans_lt` `zero_le_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne_bot` `Finset.prod_cons` `mul_coeff_zero` `coeff_zero_prod` `mul_neg` `coeff_zero_eq_eval_zero` `eval_sub` `eval_pow` `eval_X` `zero_pow` `ne_of_gt` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `eval_one`
`cyclotomic_dvd_geom_sum_of_dvd` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `semiring` `cyclotomic` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`prod_cyclotomic_eq_geom_sum` `Finset.dvd_prod_of_mem` `LT.lt.ne'` `map_cyclotomic_int` `map_sum` `Finset.sum_congr` `map_pow` `map_X` `map_dvd`
`cyclotomic_eq_X_pow_sub_one_div` 📖	mathematical	—	`cyclotomic` `CommRing.toRing` `divByMonic` `Polynomial` `Ring.toSemiring` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Nat.properDivisors`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `prod_cyclotomic_eq_X_pow_sub_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne'` `Finset.prod_cons` `monic_prod_of_monic` `cyclotomic.monic` `div_modByMonic_unique` `zero_add` `mul_comm` `bot_lt_iff_ne_bot` `Monic.ne_zero` `degree_eq_bot`
`cyclotomic_eq_prod_X_pow_sub_one_pow_moebius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Polynomial` `Ring.toSemiring` `CommRing.toRing` `RatFunc` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RatFunc.instField` `RingHom.instFunLike` `algebraMap` `RatFunc.instAlgebraOfPolynomial` `Algebra.id` `cyclotomic` `Finset.prod` `CommRing.toCommMonoid` `RatFunc.instCommRing` `Nat.divisorsAntidiagonal` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `ArithmeticFunction.instFunLikeNat` `ArithmeticFunction.moebius`	—	`cyclotomic_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finset.prod_congr` `Nat.divisorsAntidiagonal_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_pow` `prod_cyclotomic_eq_X_pow_sub_one` `map_prod` `ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero` `RatFunc.instIsFractionRingPolynomial` `IsDomain.toNontrivial` `Monic.ne_zero` `monic_X_pow_sub_C` `ne_of_gt`
`cyclotomic_eq_prod_X_sub_primitiveRoots` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`cyclotomic` `CommRing.toRing` `Finset.prod` `Polynomial` `Ring.toSemiring` `commRing` `primitiveRoots` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`cyclotomic'.eq_1` `Nat.strong_induction_on` `cyclotomic_zero` `cyclotomic'.congr_simp` `cyclotomic'_zero` `Nat.mem_properDivisors` `IsPrimitiveRoot.pow` `mul_comm` `cyclotomic_eq_X_pow_sub_one_div` `cyclotomic'_eq_X_pow_sub_one_div` `Finset.prod_congr` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`
`cyclotomic_ne_zero` 📖	—	—	—	—	`Monic.ne_zero` `cyclotomic.monic`
`cyclotomic_one` 📖	mathematical	—	`cyclotomic` `Polynomial` `Ring.toSemiring` `instSub` `X` `instOne`	—	`instIsDomain` `map_sub` `map_X` `map_one` `cyclotomic'_one` `map_cyclotomic_int` `int_cyclotomic_unique`
`cyclotomic_prime` 📖	mathematical	—	`cyclotomic` `Finset.sum` `Polynomial` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`prod_cyclotomic_eq_geom_sum` `Nat.Prime.pos` `Fact.out` `Nat.Prime.divisors` `Finset.erase_insert` `Iff.not` `Finset.mem_singleton` `Nat.Prime.ne_one` `Finset.prod_singleton` `map_cyclotomic_int` `map_sum` `Finset.sum_congr` `map_pow` `map_X`
`cyclotomic_prime_mul_X_sub_one` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `instMul` `cyclotomic` `instSub` `X` `instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`cyclotomic_prime` `geom_sum_mul`
`cyclotomic_prime_pow_eq_geom_sum` 📖	mathematical	`Nat.Prime`	`cyclotomic` `Monoid.toNatPow` `Nat.instMonoid` `CommRing.toRing` `Finset.sum` `Polynomial` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`eq_cyclotomic_iff` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.Prime.pos` `Nat.prod_properDivisors_prime_pow` `zero_add` `pow_one` `cyclotomic_prime` `Finset.sum_congr` `pow_zero` `Finset.prod_range_succ` `mul_comm` `geom_sum_mul` `pow_mul` `pow_add`
`cyclotomic_prime_pow_mul_X_pow_sub_one` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `CommRing.toRing` `instMul` `cyclotomic` `Monoid.toNatPow` `Nat.instMonoid` `instSub` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne`	—	`cyclotomic_prime_pow_eq_geom_sum` `Fact.out` `geom_sum_mul` `pow_mul` `pow_succ` `mul_comm`
`cyclotomic_three` 📖	mathematical	—	`cyclotomic` `Polynomial` `Ring.toSemiring` `instAdd` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne`	—	`cyclotomic_prime` `Nat.fact_prime_three` `Finset.sum_range_succ'` `Finset.sum_singleton` `zero_add` `pow_one` `pow_zero`
`cyclotomic_two` 📖	mathematical	—	`cyclotomic` `Polynomial` `Ring.toSemiring` `instAdd` `X` `instOne`	—	`cyclotomic_prime` `Nat.fact_prime_two` `geom_sum_two`
`cyclotomic_zero` 📖	mathematical	—	`cyclotomic` `Polynomial` `Ring.toSemiring` `instOne`	—	—
`degree_cyclotomic` 📖	mathematical	—	`degree` `Ring.toSemiring` `cyclotomic` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.totient`	—	`map_cyclotomic_int` `degree_map_eq_of_leadingCoeff_ne_zero` `Monic.leadingCoeff` `instIsDomain` `int_cyclotomic_spec` `eq_intCast` `RingHom.instRingHomClass` `Int.cast_one` `NeZero.one` `degree_one` `Int.instNontrivial` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithBot.charZero` `Nat.instCharZero` `degree_cyclotomic'` `Nat.instAtLeastTwoHAddOfNat` `Complex.isPrimitiveRoot_exp`
`degree_cyclotomic'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `cyclotomic'` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.totient`	—	`degree_eq_natDegree` `cyclotomic'_ne_zero` `natDegree_cyclotomic'`
`degree_cyclotomic_pos` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Ring.toSemiring` `cyclotomic`	—	`degree_cyclotomic` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instNontrivial` `Nat.cast_pos` `WithBot.instIsOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `WithBot.nontrivial` `Nat.totient_pos`
`dvd_C_mul_X_sub_one_pow_add_one` 📖	mathematical	`Nat.Prime` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	`Polynomial` `commRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instAdd` `instSub` `instMul` `X` `instOne`	—	`Nat.Prime.dvd_add_pow_sub_pow_of_dvd` `mul_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Dvd.dvd.trans` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_mul` `map_natCast` `sub_neg_eq_add` `one_pow` `Odd.neg_pow` `Nat.Prime.odd_of_ne_two` `sub_eq_add_neg`
`eq_cyclotomic_iff` 📖	mathematical	—	`cyclotomic` `CommRing.toRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `instMul` `Finset.prod` `CommRing.toCommMonoid` `commRing` `Nat.properDivisors` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `prod_cyclotomic_eq_X_pow_sub_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne'` `Finset.prod_cons` `monic_prod_of_monic` `cyclotomic.monic` `cyclotomic_eq_X_pow_sub_one_div` `div_modByMonic_unique` `zero_add` `mul_comm` `degree_zero` `bot_lt_iff_ne_bot` `Monic.ne_zero` `degree_eq_bot`
`int_coeff_of_cyclotomic'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`map` `Int.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `cyclotomic'` `degree` `Monic`	—	`lifts_and_degree_eq_and_monic` `IsDomain.toNontrivial` `Nat.strong_induction_on` `map_one` `cyclotomic'_zero` `monic_prod_of_monic` `cyclotomic'.monic` `Subsemiring.prod_mem` `Nat.mem_properDivisors` `IsPrimitiveRoot.pow` `mul_comm` `zero_add` `prod_cyclotomic'_eq_X_pow_sub_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne'` `Finset.prod_cons` `Monic.ne_zero` `div_modByMonic_unique` `coe_mapRingHom` `map_divByMonic` `map_sub` `map_pow` `map_X`
`int_cyclotomic_rw` 📖	mathematical	—	`cyclotomic` `Int.instRing` `Polynomial` `Int.instSemiring` `Complex` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Complex.commRing` `map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `cyclotomic'` `instIsDomain` `Field.toSemifield` `Complex.instField` `WithBot` `degree` `Monic` `int_coeff_of_cyclotomic'` `Complex.exp` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Complex.isPrimitiveRoot_exp`	—	`instIsDomain` `int_coeff_of_cyclotomic'` `Nat.instAtLeastTwoHAddOfNat` `Complex.isPrimitiveRoot_exp` `ext` `coeff_map` `eq_intCast` `RingHom.instRingHomClass`
`int_cyclotomic_spec` 📖	mathematical	—	`map` `Complex` `Int.instSemiring` `Complex.instSemiring` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Complex.commRing` `cyclotomic` `Int.instRing` `cyclotomic'` `instIsDomain` `Field.toSemifield` `Complex.instField` `degree` `Ring.toSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monic`	—	`instIsDomain` `cyclotomic'.congr_simp` `cyclotomic'_zero` `degree_one` `Complex.instNontrivial` `map_one` `Int.instNontrivial` `int_coeff_of_cyclotomic'` `Nat.instAtLeastTwoHAddOfNat` `Complex.isPrimitiveRoot_exp` `int_cyclotomic_rw`
`int_cyclotomic_unique` 📖	mathematical	`map` `Complex` `Int.instSemiring` `Complex.instSemiring` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Complex.commRing` `cyclotomic'` `instIsDomain` `Field.toSemifield` `Complex.instField`	`cyclotomic` `Int.instRing`	—	`instIsDomain` `map_injective` `Int.cast_injective` `Complex.instCharZero` `int_cyclotomic_spec`
`map_cyclotomic` 📖	mathematical	—	`map` `Ring.toSemiring` `cyclotomic`	—	`map_cyclotomic_int` `map_map` `RingHom.Int.subsingleton_ringHom` `Lean.Meta.FastSubsingleton.elim`
`map_cyclotomic_int` 📖	mathematical	—	`map` `Int.instSemiring` `Ring.toSemiring` `Int.castRingHom` `Ring.toNonAssocRing` `cyclotomic` `Int.instRing`	—	`cyclotomic'.congr_simp` `map_one` `Int.castRingHom_int` `map_id`
`natDegree_cyclotomic` 📖	mathematical	—	`natDegree` `Ring.toSemiring` `cyclotomic` `Nat.totient`	—	`natDegree.eq_1` `degree_cyclotomic`
`natDegree_cyclotomic'` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `cyclotomic'` `Nat.totient`	—	`cyclotomic'.eq_1` `natDegree_prod` `IsDomain.to_noZeroDivisors` `X_sub_C_ne_zero` `IsDomain.toNontrivial` `Finset.sum_congr` `natDegree_X_sub_C` `Finset.sum_const` `IsPrimitiveRoot.card_primitiveRoots` `nsmul_eq_mul` `mul_one`
`natDegree_cyclotomic_le` 📖	mathematical	—	`natDegree` `Ring.toSemiring` `cyclotomic` `Nat.totient`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `natDegree_of_subsingleton` `Nat.instCanonicallyOrderedAdd` `natDegree_cyclotomic` `le_refl`
`orderOf_root_cyclotomic_dvd` 📖	mathematical	`IsRoot` `ZMod` `Ring.toSemiring` `CommRing.toRing` `ZMod.commRing` `cyclotomic` `DFunLike.coe` `RingHom` `Nat.instNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Nat.castRingHom`	`orderOf` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instMonoid` `ZMod.unitOfCoprime` `coprime_of_root_cyclotomic`	—	`orderOf_dvd_of_pow_eq_one` `coprime_of_root_cyclotomic` `prod_cyclotomic_eq_X_pow_sub_one` `Nat.self_notMem_properDivisors` `Nat.cons_self_properDivisors` `LT.lt.ne'` `Finset.prod_cons` `eval_mul` `IsRoot.def` `MulZeroClass.zero_mul` `Units.val_eq_one` `sub_eq_zero` `eq_natCast` `RingHom.instRingHomClass` `eval_sub` `eval_pow` `eval_X` `eval_one`
`prod_cyclotomic'_eq_X_pow_sub_one` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid`	`Finset.prod` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Nat.divisors` `cyclotomic'` `instSub` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne`	—	`IsPrimitiveRoot.disjoint` `Finset.prod_congr` `Finset.prod_biUnion` `X_pow_sub_one_eq_prod` `IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots`
`prod_cyclotomic_eq_X_pow_sub_one` 📖	mathematical	—	`Finset.prod` `Polynomial` `Ring.toSemiring` `CommRing.toRing` `CommRing.toCommMonoid` `commRing` `Nat.divisors` `cyclotomic` `instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instOne`	—	`map_injective` `Int.cast_injective` `Complex.instCharZero` `instIsDomain` `map_prod` `Finset.prod_congr` `map_sub` `map_pow` `map_X` `map_one` `prod_cyclotomic'_eq_X_pow_sub_one` `Nat.instAtLeastTwoHAddOfNat` `Complex.isPrimitiveRoot_exp` `LT.lt.ne'` `map_cyclotomic_int`
`prod_cyclotomic_eq_geom_sum` 📖	mathematical	—	`Finset.prod` `Polynomial` `Ring.toSemiring` `CommRing.toRing` `CommRing.toCommMonoid` `commRing` `Finset.erase` `Nat.divisors` `cyclotomic` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`mul_left_inj'` `instIsRightCancelMulZeroOfIsCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `IsCancelMulZero.toIsRightCancelMulZero` `Int.instIsCancelMulZero` `cyclotomic_ne_zero` `Int.instNontrivial` `Finset.prod_erase_mul` `Nat.one_mem_divisors` `LT.lt.ne'` `cyclotomic_one` `geom_sum_mul` `prod_cyclotomic_eq_X_pow_sub_one` `map_prod` `Finset.prod_congr` `map_cyclotomic_int` `map_sum` `Finset.sum_congr` `map_pow` `map_X`
`roots_of_cyclotomic` 📖	mathematical	—	`roots` `cyclotomic'` `Finset.val` `primitiveRoots`	—	`cyclotomic'.eq_1` `roots_prod_X_sub_C`
`separable_cyclotomic` 📖	mathematical	—	`Separable` `Semifield.toCommSemiring` `Field.toSemifield` `cyclotomic` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Separable.of_dvd` `separable_X_pow_sub_C` `one_ne_zero` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `cyclotomic.dvd_X_pow_sub_one`
`squarefree_cyclotomic` 📖	mathematical	—	`Squarefree` `Polynomial` `Ring.toSemiring` `DivisionRing.toRing` `Field.toDivisionRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `cyclotomic`	—	`Separable.squarefree` `separable_cyclotomic`
`unique_int_coeff_of_cycl` 📖	mathematical	`IsPrimitiveRoot` `CommRing.toCommMonoid` `PNat.val`	`ExistsUnique` `Polynomial` `Int.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `cyclotomic'`	—	`int_coeff_of_cyclotomic'` `map_injective` `Int.cast_injective`

Polynomial.cyclotomic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_X_pow_sub_one` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `Polynomial.semiring` `Polynomial.cyclotomic` `Polynomial.instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.X` `Polynomial.instOne`	—	`Polynomial.cyclotomic_zero` `pow_zero` `sub_self` `Polynomial.prod_cyclotomic_eq_X_pow_sub_one` `Finset.dvd_prod_of_mem` `Nat.mem_divisors_self` `LT.lt.ne'` `Polynomial.map_cyclotomic_int` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.map_one` `Polynomial.map_dvd`
`eval_apply` 📖	mathematical	—	`Polynomial.eval` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.cyclotomic`	—	`Polynomial.map_cyclotomic` `Polynomial.eval_map` `Polynomial.eval₂_at_apply`
`eval_apply_ofReal` 📖	mathematical	—	`Polynomial.eval` `Complex` `Ring.toSemiring` `Complex.instRing` `Complex.ofReal` `Polynomial.cyclotomic` `Real` `Real.instRing`	—	`eval_apply`
`isPrimitive` 📖	mathematical	—	`Polynomial.IsPrimitive` `CommRing.toCommSemiring` `Polynomial.cyclotomic` `CommRing.toRing`	—	`Polynomial.Monic.isPrimitive` `monic`
`monic` 📖	mathematical	—	`Polynomial.Monic` `Ring.toSemiring` `Polynomial.cyclotomic`	—	`Polynomial.map_cyclotomic_int` `Polynomial.Monic.map` `instIsDomain` `Polynomial.int_cyclotomic_spec`

Polynomial.cyclotomic'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monic` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.cyclotomic'`	—	`Polynomial.monic_prod_of_monic` `Polynomial.monic_X_sub_C`

---

← Back to Index