MinpolyDiv

📁 Source: Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Statistics

Metric	Count
Definitions minpolyDiv	1
Theorems coeff_minpolyDiv, coeff_minpolyDiv_mem_adjoin, coeff_minpolyDiv_sub_pow_mem_span, eval_minpolyDiv_of_aeval_eq_zero, eval_minpolyDiv_self, eval₂_minpolyDiv_of_eval₂_eq_zero, eval₂_minpolyDiv_self, minpolyDiv_eq_of_isIntegrallyClosed, minpolyDiv_eq_zero, minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero, minpolyDiv_monic, minpolyDiv_ne_zero, minpolyDiv_spec, natDegree_minpolyDiv, natDegree_minpolyDiv_lt, natDegree_minpolyDiv_succ, span_coeff_minpolyDiv, sum_smul_minpolyDiv_eq_X_pow	18
Total	19

(root)

Definitions

Name	Category	Theorems
minpolyDiv 📖	CompOp	18 math math: eval_minpolyDiv_self, eval₂_minpolyDiv_self, eval₂_minpolyDiv_of_eval₂_eq_zero, natDegree_minpolyDiv_succ, sum_smul_minpolyDiv_eq_X_pow, eval_minpolyDiv_of_aeval_eq_zero, coeff_minpolyDiv_sub_pow_mem_span, minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero, span_coeff_minpolyDiv, natDegree_minpolyDiv_lt, coeff_minpolyDiv_mem_adjoin, coeff_minpolyDiv, minpolyDiv_eq_of_isIntegrallyClosed, minpolyDiv_spec, minpolyDiv_eq_zero, Module.Basis.traceDual_powerBasis_eq, minpolyDiv_monic, natDegree_minpolyDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_minpolyDiv 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap minpoly CommRing.toRing Distrib.toMul	—	Polynomial.coeff_map minpolyDiv_spec mul_sub Polynomial.coeff_sub Polynomial.coeff_mul_X Polynomial.coeff_mul_C sub_add_cancel
coeff_minpolyDiv_mem_adjoin 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Polynomial.coeff minpolyDiv	—	coeff_minpolyDiv AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass Subalgebra.algebraMap_mem MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass Algebra.self_mem_adjoin_singleton Polynomial.coeff_eq_zero_of_natDegree_lt ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass
coeff_minpolyDiv_sub_pow_mem_span 📖	mathematical	IsIntegral CommRing.toRing Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.image Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set.Iio Nat.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.coeff minpolyDiv Polynomial.natDegree	—	IsMin.Iio_eq Set.image_empty Submodule.span_empty tsub_zero Nat.instOrderedSub Polynomial.Monic.leadingCoeff minpolyDiv_monic pow_zero sub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass coeff_minpolyDiv add_sub_assoc pow_succ sub_mul Algebra.algebraMap_eq_smul_one AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.smul_mem Submodule.subset_span tsub_tsub tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_tsub_of_add_le_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsScalarTower.right SetLike.le_def instIsConcreteLE Submodule.span_mul_span Set.mul_singleton Set.image_image Submodule.span_mono Set.mem_Iio Submodule.mul_mem_mul LE.le.trans Submodule.mem_span_singleton_self
eval_minpolyDiv_of_aeval_eq_zero 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.eval.eq_1 eval₂_minpolyDiv_of_eval₂_eq_zero RingHomCompTriple.comp_eq RingHomCompTriple.right_ids RingHom.id_apply
eval_minpolyDiv_self 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly CommRing.toRing	—	Polynomial.eval_map_algebraMap Polynomial.derivative_map minpolyDiv_spec Polynomial.derivative_mul Polynomial.derivative_sub Polynomial.derivative_X Polynomial.derivative_C sub_zero mul_one Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C sub_self MulZeroClass.mul_zero zero_add
eval₂_minpolyDiv_of_eval₂_eq_zero 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHom.comp Semiring.toNonAssocSemiring algebraMap minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.eval₂_hom eval_minpolyDiv_self Polynomial.eval₂_mul Polynomial.eval₂_sub Polynomial.eval₂_X Polynomial.eval₂_C IsDomain.to_noZeroDivisors minpolyDiv_spec Polynomial.eval₂_map
eval₂_minpolyDiv_self 📖	mathematical	—	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass DFunLike.coe minpolyDiv Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id Polynomial.aeval LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eval₂_minpolyDiv_of_eval₂_eq_zero AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp_algebraMap Polynomial.eval₂_map RingHom.coe_coe Polynomial.eval₂_hom Polynomial.eval_map_algebraMap minpoly.aeval map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
minpolyDiv_eq_of_isIntegrallyClosed 📖	mathematical	IsIntegral CommRing.toRing	minpolyDiv EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsScalarTower.algebraMap_eq Polynomial.map_map minpoly.isIntegrallyClosed_eq_field_fractions'
minpolyDiv_eq_zero 📖	mathematical	IsIntegral CommRing.toRing	minpolyDiv Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	Polynomial.map_zero Polynomial.zero_divByMonic
minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval minpoly CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.eval_mul Polynomial.eval_sub Polynomial.eval_X Polynomial.eval_C IsDomain.to_noZeroDivisors minpolyDiv_spec Polynomial.eval_map_algebraMap sub_eq_zero
minpolyDiv_monic 📖	mathematical	IsIntegral CommRing.toRing	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim minpolyDiv_spec Polynomial.leadingCoeff_X_sub_C mul_one Polynomial.Monic.leadingCoeff Polynomial.Monic.map minpoly.monic Polynomial.leadingCoeff_mul' minpolyDiv_ne_zero
minpolyDiv_ne_zero 📖	—	IsIntegral CommRing.toRing	—	—	minpolyDiv_spec Polynomial.Monic.ne_zero Polynomial.Monic.map minpoly.monic MulZeroClass.zero_mul
minpolyDiv_spec 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul minpolyDiv Polynomial.instSub CommRing.toRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.map algebraMap minpoly	—	mul_comm Polynomial.mul_divByMonic_eq_iff_isRoot Polynomial.IsRoot.eq_1 Polynomial.eval_map_algebraMap minpoly.aeval
natDegree_minpolyDiv 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv minpoly CommRing.toRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Polynomial.natDegree_of_subsingleton minpoly.subsingleton Polynomial.natDegree_one zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub natDegree_minpolyDiv_succ minpolyDiv_eq_zero minpoly.eq_zero
natDegree_minpolyDiv_lt 📖	mathematical	IsIntegral CommRing.toRing	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv minpoly CommRing.toRing	—	natDegree_minpolyDiv_succ
natDegree_minpolyDiv_succ 📖	mathematical	IsIntegral CommRing.toRing	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring minpolyDiv minpoly CommRing.toRing	—	Polynomial.Monic.natDegree_map minpoly.monic minpolyDiv_spec Polynomial.natDegree_mul' Polynomial.leadingCoeff_X_sub_C mul_one minpolyDiv_ne_zero Polynomial.natDegree_sub_C Polynomial.natDegree_X
span_coeff_minpolyDiv 📖	mathematical	IsIntegral CommRing.toRing	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Set.range Polynomial.coeff minpolyDiv DFunLike.coe OrderEmbedding Subalgebra Submodule NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule Algebra.adjoin Set Set.instSingletonSet	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton le_antisymm Submodule.span_le coeff_minpolyDiv_mem_adjoin Submodule.span_range_natDegree_eq_adjoin minpoly.monic minpoly.aeval Finset.coe_image Finset.coe_range Submodule.subset_span Set.mem_range_self Set.mem_preimage SetLike.mem_coe Submodule.sub_mem_iff_right SetLike.le_def instIsConcreteLE Set.image_subset_iff lt_trans coeff_minpolyDiv_sub_pow_mem_span Set.mem_Iio natDegree_minpolyDiv_succ
sum_smul_minpolyDiv_eq_X_pow 📖	mathematical	Algebra.adjoin Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set Set.instSingletonSet Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	Finset.sum AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.univ minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing instIsDomain Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.toSMul Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe Polynomial.aeval LinearMap RingHom.id NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative minpoly minpolyDiv Polynomial.X	—	instIsDomain AlgHomClass.toRingHomClass AlgHom.algHomClass sub_eq_zero AlgHom.ext_of_adjoin_eq_top Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero Finset.sum_congr Polynomial.map_smul map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass Polynomial.eval_sub Polynomial.eval_finset_sum Polynomial.eval_smul IsScalarTower.right Polynomial.eval_map eval₂_minpolyDiv_self mul_ite MulZeroClass.mul_zero Finset.sum_ite_eq' Polynomial.eval_X_pow div_mul_cancel₀ map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.Separable.aeval_derivative_ne_zero Algebra.IsSeparable.isSeparable minpoly.aeval LE.le.trans_lt Polynomial.natDegree_sub_le max_lt Polynomial.natDegree_sum_le Finset.fold_congr AlgHom.card Module.finrank_pos commRing_strongRankCondition instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LE.le.trans Polynomial.natDegree_smul_le Polynomial.natDegree_map_le LT.lt.trans_le natDegree_minpolyDiv_lt Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral Algebra.IsSeparable.isAlgebraic minpoly.natDegree_le Polynomial.natDegree_pow IsDomain.to_noZeroDivisors Polynomial.natDegree_X mul_one

---

← Back to Index