Minpoly

📁 Source: Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

Statistics

Metric	Count
Definitions	0
Theorems isIntegral, is_roots_of_minpoly, minpoly_dvd_expand, minpoly_dvd_mod_p, minpoly_dvd_pow_mod, minpoly_dvd_x_pow_sub_one, minpoly_eq_pow, minpoly_eq_pow_coprime, pow_isRoot_minpoly, separable_minpoly_mod, squarefree_minpoly_mod, totient_le_degree_minpoly	12
Total	12

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	IsIntegral Int.instCommRing CommRing.toRing Ring.toIntAlgebra	—	Polynomial.monic_X_pow_sub_C ne_of_lt Polynomial.eval₂_sub Polynomial.eval₂_X_pow iff_def Polynomial.eval₂_one sub_self
is_roots_of_minpoly 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Finset Finset.instHasSubset primitiveRoots Multiset.toFinset Polynomial.roots Polynomial.map Int.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra	—	primitiveRoots.congr_simp primitiveRoots_zero isPrimitiveRoot_iff mem_primitiveRoots Polynomial.mem_roots Polynomial.map_monic_ne_zero minpoly.monic isIntegral instNontrivialOfCharZero pow_isRoot_minpoly
minpoly_dvd_expand 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing minpoly CommRing.toRing Ring.toIntAlgebra DFunLike.coe AlgHom Int.instCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.expand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	minpoly.isIntegrallyClosed_dvd Int.instIsDomain GCDMonoid.toIsIntegrallyClosed IsBezout.nonemptyGCDMonoid IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero isIntegral Polynomial.aeval_def Polynomial.coe_expand Polynomial.comp.eq_1 Polynomial.eval₂_eq_eval_map Polynomial.map_comp Polynomial.map_pow Polynomial.map_X Polynomial.eval_comp Polynomial.eval_X_pow minpoly.aeval
minpoly_dvd_mod_p 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing ZMod.commRing Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	Squarefree.isRadical UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd ZMod.instIsDomain EuclideanDomain.to_principal_ideal_domain squarefree_minpoly_mod minpoly_dvd_pow_mod
minpoly_dvd_pow_mod 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing ZMod.commRing Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	ZMod.expand_card Polynomial.map_expand map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass minpoly_dvd_expand
minpoly_dvd_x_pow_sub_one 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing minpoly CommRing.toRing Ring.toIntAlgebra Polynomial.instSub Int.instRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.instOne	—	pow_zero sub_self minpoly.isIntegrallyClosed_dvd Int.instIsDomain IsIntegralClosure.of_isIntegrallyClosed Localization.isLocalization GCDMonoid.toIsIntegrallyClosed IsBezout.nonemptyGCDMonoid IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain OreLocalization.instIsScalarTower IsScalarTower.right Algebra.IsIntegral.of_finite AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero isIntegral map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_X_pow iff_def Polynomial.aeval_one
minpoly_eq_pow 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	minpoly.monic isIntegral pow_of_prime Fact.out minpoly.irreducible Int.instIsDomain Polynomial.IsPrimitive.mul Polynomial.Monic.isPrimitive Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast Polynomial.monic_X_pow_sub_C ne_of_gt Polynomial.map_mul IsCoprime.mul_dvd Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast dvd_or_isCoprime IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain Polynomial.map_dvd_map Int.cast_injective Rat.instCharZero Polynomial.eq_of_monic_of_associated associated_of_dvd_dvd Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsCancelMulZero.toIsLeftCancelMulZero Int.instIsCancelMulZero Irreducible.dvd_symm minpoly_dvd_x_pow_sub_one map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass minpoly_dvd_mod_p lt_of_lt_of_le Nat.instAtLeastTwoHAddOfNat Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid le_emultiplicity_of_pow_dvd dvd_trans Polynomial.map_pow sq mul_assoc Polynomial.map_X Polynomial.map_one Polynomial.map_sub Polynomial.coe_mapRingHom Polynomial.Separable.squarefree Polynomial.separable_X_pow_sub_C ZMod.natCast_eq_zero_iff one_ne_zero NeZero.one ZMod.nontrivial Nat.Prime.one_lt' squarefree_iff_emultiplicity_le_one LE.le.not_gt Nat.cast_one Polynomial.degree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors ZMod.instIsDomain LT.lt.ne' minpoly.degree_pos instNontrivialOfCharZero Polynomial.degree_map_eq_of_leadingCoeff_ne_zero Polynomial.Monic.leadingCoeff eq_intCast Int.cast_one
minpoly_eq_pow_coprime 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	UniqueFactorizationMonoid.induction_on_prime Nat.instUniqueFactorizationMonoid pow_zero Nat.isUnit_iff pow_one Prime.nat_prime Nat.Prime.coprime_iff_not_dvd minpoly_eq_pow pow_of_coprime Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr
pow_isRoot_minpoly 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	minpoly_eq_pow_coprime Polynomial.eval_map minpoly.aeval
separable_minpoly_mod 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Polynomial.Separable ZMod Semifield.toCommSemiring Field.toSemifield ZMod.instField Polynomial.map Int.instSemiring CommSemiring.toSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.map_X map_one MonoidHomClass.toOneHomClass map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass minpoly_dvd_x_pow_sub_one Polynomial.Separable.of_dvd Polynomial.separable_X_pow_sub_C ZMod.natCast_eq_zero_iff one_ne_zero NeZero.one ZMod.nontrivial Nat.Prime.one_lt'
squarefree_minpoly_mod 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Squarefree Polynomial ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map Int.instSemiring Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing ZMod.commRing minpoly Int.instCommRing CommRing.toRing Ring.toIntAlgebra	—	Polynomial.Separable.squarefree separable_minpoly_mod
totient_le_degree_minpoly 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	Nat.totient Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing minpoly CommRing.toRing Ring.toIntAlgebra	—	card_primitiveRoots Finset.card_le_card is_roots_of_minpoly Multiset.toFinset_card_le Polynomial.card_roots' Polynomial.natDegree_map_le

---

← Back to Index