Roots

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

Statistics

Metric	Count
Definitions	0
Theorems isRoot_cyclotomic, minpoly_dvd_cyclotomic, minpoly_eq_cyclotomic_of_irreducible, sum_eq_zero_iff_forall_eq, sum_eq_zero_iff_forall_eq_int, irreducible, irreducible_rat, isCoprime_rat, roots_eq_primitiveRoots_val, roots_to_finset_eq_primitiveRoots, cyclotomic_eq_minpoly, cyclotomic_eq_minpoly_rat, cyclotomic_injective, isRoot_cyclotomic_iff, isRoot_cyclotomic_iff_charZero, isRoot_of_unity_of_root_cyclotomic, roots_cyclotomic_nodup, isRoot_of_unity_iff	18
Total	18

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRoot_cyclotomic 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial.IsRoot Ring.toSemiring CommRing.toRing Polynomial.cyclotomic	—	Polynomial.mem_roots Polynomial.cyclotomic_ne_zero IsDomain.toNontrivial Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots Polynomial.roots_prod_X_sub_C Finset.mem_def mem_primitiveRoots
minpoly_dvd_cyclotomic 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing minpoly DivisionRing.toRing Field.toDivisionRing Ring.toIntAlgebra Polynomial.cyclotomic Int.instRing	—	minpoly.isIntegrallyClosed_dvd Int.instIsDomain IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero isIntegral Polynomial.eval₂_eq_eval_map Polynomial.map_cyclotomic isRoot_cyclotomic
minpoly_eq_cyclotomic_of_irreducible 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid Irreducible Polynomial Ring.toSemiring DivisionRing.toRing Field.toDivisionRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.cyclotomic	minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing	—	minpoly.eq_of_irreducible_of_monic IsDomain.toNontrivial Polynomial.aeval_def Polynomial.eval₂_eq_eval_map Polynomial.map_cyclotomic Polynomial.IsRoot.def Polynomial.isRoot_cyclotomic_iff NeZero.of_faithfulSMul IsScalarTower.right instFaithfulSMul_1 DivisionRing.isSimpleRing Polynomial.cyclotomic.monic
sum_eq_zero_iff_forall_eq 📖	mathematical	Nat.Prime IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DivisionRing.toRatCast Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Polynomial.finset_sum_coeff Finset.sum_congr Polynomial.coeff_C_mul Polynomial.coeff_X_pow mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq LE.le.trans Polynomial.degree_sum_le Finset.sup_le le_imp_le_of_le_of_le Polynomial.degree_C_mul_X_pow_le le_refl WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass Polynomial.aeval_C eq_ratCast RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X minpoly.dvd_iff Polynomial.cyclotomic_eq_minpoly_rat Nat.Prime.pos WithBot.add_le_add_iff_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le add_zero Nat.totient_prime Polynomial.degree_cyclotomic Rat.nontrivial Polynomial.degree_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Polynomial.natDegree_eq_zero Polynomial.natDegree_eq_zero_iff_degree_le_zero Polynomial.cyclotomic_prime Polynomial.coeff_mul_C one_mul NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Polynomial.ext CanLift.prf Fin.instCanLiftNatValLt Finset.sum_eq_zero instIsEmptyFalse MulZeroClass.zero_mul
sum_eq_zero_iff_forall_eq_int 📖	mathematical	Nat.Prime IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finset.sum_congr Rat.cast_intCast Rat.instCharZero sum_eq_zero_iff_forall_eq

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclotomic_eq_minpoly 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	cyclotomic Int.instRing minpoly Int.instCommRing DivisionRing.toRing Field.toDivisionRing Ring.toIntAlgebra	—	eq_of_monic_of_dvd_of_natDegree_le minpoly.monic IsPrimitiveRoot.isIntegral cyclotomic.monic IsPrimitiveRoot.minpoly_dvd_cyclotomic natDegree_cyclotomic Int.instNontrivial IsPrimitiveRoot.totient_le_degree_minpoly instIsDomain
cyclotomic_eq_minpoly_rat 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	cyclotomic NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField minpoly Rat.commRing DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatAlgebra	—	map_cyclotomic_int cyclotomic_eq_minpoly minpoly.isIntegrallyClosed_eq_field_fractions' Int.instIsDomain Rat.isFractionRing IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsDomain AddCommGroup.intIsScalarTower IsPrimitiveRoot.isIntegral
cyclotomic_injective 📖	mathematical	—	Polynomial Ring.toSemiring CommRing.toRing cyclotomic	—	eq_or_ne cyclotomic_zero Nat.totient_eq_zero natDegree_cyclotomic instNontrivialOfCharZero natDegree_one map_injective Int.cast_injective map_cyclotomic_int Nat.instAtLeastTwoHAddOfNat Complex.isPrimitiveRoot_exp isRoot_cyclotomic_iff instIsDomain NeZero.charZero Complex.instCharZero IsPrimitiveRoot.eq_orderOf eval_one NeZero.one Complex.instNontrivial
isRoot_cyclotomic_iff 📖	mathematical	—	IsRoot Ring.toSemiring CommRing.toRing cyclotomic IsPrimitiveRoot CommRing.toCommMonoid	—	IsFractionRing.injective Localization.isLocalization isRoot_map_iff IsPrimitiveRoot.map_iff_of_injective MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_cyclotomic NeZero.nat_of_injective
isRoot_cyclotomic_iff_charZero 📖	mathematical	—	IsRoot Ring.toSemiring CommRing.toRing cyclotomic IsPrimitiveRoot CommRing.toCommMonoid	—	isRoot_cyclotomic_iff NeZero.charZero NeZero.of_gt Nat.instCanonicallyOrderedAdd
isRoot_of_unity_of_root_cyclotomic 📖	mathematical	Finset Finset.instMembership Nat.divisors IsRoot Ring.toSemiring CommRing.toRing cyclotomic	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	pow_zero prod_cyclotomic_eq_X_pow_sub_one eval_eq_zero_of_dvd_of_eval_eq_zero Finset.dvd_prod_of_mem add_zero eq_add_of_sub_eq' eval_one eval_X_pow eval_sub
roots_cyclotomic_nodup 📖	mathematical	—	Multiset.Nodup roots cyclotomic CommRing.toRing	—	Multiset.empty_or_exists_mem Multiset.nodup_zero Multiset.nodup_of_le roots.le_of_dvd X_pow_sub_C_ne_zero IsDomain.toNontrivial NeZero.pos_of_neZero_natCast cyclotomic.dvd_X_pow_sub_one IsPrimitiveRoot.nthRoots_one_nodup isRoot_cyclotomic_iff mem_roots cyclotomic_ne_zero

Polynomial.cyclotomic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irreducible 📖	mathematical	—	Irreducible Polynomial Ring.toSemiring Int.instRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.cyclotomic	—	Nat.instAtLeastTwoHAddOfNat Polynomial.cyclotomic_eq_minpoly Complex.isPrimitiveRoot_exp LT.lt.ne' Complex.instCharZero minpoly.irreducible Int.instIsDomain instIsDomain IsPrimitiveRoot.isIntegral
irreducible_rat 📖	mathematical	—	Irreducible Polynomial Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.cyclotomic	—	Polynomial.map_cyclotomic_int Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map Rat.isFractionRing Int.instIsDomain instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain isPrimitive irreducible
isCoprime_rat 📖	mathematical	—	IsCoprime Polynomial Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Polynomial.commSemiring Rat.commSemiring Polynomial.cyclotomic	—	isCoprime_one_left isCoprime_one_right Irreducible.coprime_iff_not_dvd IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain irreducible_rat Polynomial.cyclotomic_injective Rat.instCharZero Polynomial.eq_of_monic_of_associated monic Irreducible.associated_of_dvd
roots_eq_primitiveRoots_val 📖	mathematical	—	Polynomial.roots Polynomial.cyclotomic CommRing.toRing Finset.val primitiveRoots	—	Polynomial.roots_cyclotomic_nodup roots_to_finset_eq_primitiveRoots
roots_to_finset_eq_primitiveRoots 📖	mathematical	—	Polynomial.roots Polynomial.cyclotomic CommRing.toRing Polynomial.roots_cyclotomic_nodup primitiveRoots	—	Finset.ext Polynomial.roots_cyclotomic_nodup Polynomial.cyclotomic_ne_zero IsDomain.toNontrivial NeZero.pos_of_neZero_natCast

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRoot_of_unity_iff 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Finset Finset.instMembership Nat.divisors Polynomial.IsRoot Ring.toSemiring Polynomial.cyclotomic	—	Polynomial.mem_nthRoots Polynomial.nthRoots.eq_1 Polynomial.mem_roots Polynomial.X_pow_sub_C_ne_zero IsDomain.toNontrivial Polynomial.C_1 Polynomial.prod_cyclotomic_eq_X_pow_sub_one Polynomial.isRoot_prod

---

← Back to Index