AnnihilatingPolynomial

📁 Source: Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean

Statistics

Metric	Count
Definitions annIdeal, annIdealGenerator	2
Theorems annIdealGenerator_aeval_eq_zero, annIdealGenerator_eq_minpoly, annIdealGenerator_eq_zero_iff, annIdealGenerator_mem, degree_annIdealGenerator_le_of_mem, mem_annIdeal_iff_aeval_eq_zero, mem_iff_annIdealGenerator_dvd, mem_iff_eq_smul_annIdealGenerator, monic_annIdealGenerator, monic_generator_eq_minpoly, span_minpoly_eq_annihilator, span_singleton_annIdealGenerator	12
Total	14

Polynomial

Definitions

Name	Category	Theorems
annIdeal 📖	CompOp	6 math math: mem_iff_eq_smul_annIdealGenerator, span_singleton_annIdealGenerator, annIdealGenerator_mem, mem_annIdeal_iff_aeval_eq_zero, mem_iff_annIdealGenerator_dvd, annIdealGenerator_eq_zero_iff
annIdealGenerator 📖	CompOp	10 math math: mem_iff_eq_smul_annIdealGenerator, span_singleton_annIdealGenerator, annIdealGenerator_mem, mem_iff_annIdealGenerator_dvd, annIdealGenerator_aeval_eq_zero, degree_annIdealGenerator_le_of_mem, annIdealGenerator_eq_minpoly, monic_generator_eq_minpoly, monic_annIdealGenerator, annIdealGenerator_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
annIdealGenerator_aeval_eq_zero 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield semiring Ring.toSemiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval annIdealGenerator MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	mem_annIdeal_iff_aeval_eq_zero annIdealGenerator_mem
annIdealGenerator_eq_minpoly 📖	mathematical	—	annIdealGenerator minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain	—	minpoly.eq_zero Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Ideal.mem_bot annIdealGenerator_eq_zero_iff mem_annIdeal_iff_aeval_eq_zero minpoly.unique monic_annIdealGenerator annIdealGenerator_aeval_eq_zero degree_annIdealGenerator_le_of_mem
annIdealGenerator_eq_zero_iff 📖	mathematical	—	annIdealGenerator Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instZero annIdeal Semifield.toCommSemiring Ring.toSemiring Bot.bot Ideal CommSemiring.toSemiring semiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsPrincipalIdealRing.principal EuclideanDomain.to_principal_ideal_domain instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
annIdealGenerator_mem 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal CommSemiring.toSemiring Semifield.toCommSemiring semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annIdeal Ring.toSemiring annIdealGenerator	—	Ideal.mul_mem_right Ideal.instIsTwoSided_1 Submodule.IsPrincipal.generator_mem
degree_annIdealGenerator_le_of_mem 📖	mathematical	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal CommSemiring.toSemiring Semifield.toCommSemiring semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annIdeal Ring.toSemiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree annIdealGenerator	—	degree_le_of_dvd IsDomain.to_noZeroDivisors instIsDomain mem_iff_annIdealGenerator_dvd
mem_annIdeal_iff_aeval_eq_zero 📖	mathematical	—	Polynomial CommSemiring.toSemiring Ideal semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annIdeal DFunLike.coe AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
mem_iff_annIdealGenerator_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal CommSemiring.toSemiring Semifield.toCommSemiring semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annIdeal Ring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing EuclideanDomain.toCommRing Field.toEuclideanDomain annIdealGenerator	—	Ideal.mem_span_singleton span_singleton_annIdealGenerator
mem_iff_eq_smul_annIdealGenerator 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal CommSemiring.toSemiring Semifield.toCommSemiring semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule annIdeal Ring.toSemiring Algebra.toSMul commSemiring Algebra.id annIdealGenerator	—	span_singleton_annIdealGenerator
monic_annIdealGenerator 📖	mathematical	—	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield annIdealGenerator	—	monic_mul_leadingCoeff_inv mul_ne_zero_iff instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain
monic_generator_eq_minpoly 📖	mathematical	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal.span Polynomial semiring Set Set.instSingletonSet annIdeal Semifield.toCommSemiring Ring.toSemiring	annIdealGenerator	—	annIdealGenerator_eq_zero_iff Ideal.span_singleton_eq_bot eq_of_monic_of_associated monic_annIdealGenerator Associated.ne_zero_iff Ideal.span_singleton_eq_span_singleton instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain span_singleton_annIdealGenerator
span_minpoly_eq_annihilator 📖	mathematical	—	Ideal.span Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain semiring Set Set.instSingletonSet minpoly Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.annihilator Module.AEval' Module.AEval.instAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instSemiring Module.End.applyModule Module.AEval.instModulePolynomial	—	smulCommClass_self IsScalarTower.left annIdealGenerator_eq_minpoly span_singleton_annIdealGenerator Ideal.ext mem_annIdeal_iff_aeval_eq_zero DFunLike.ext_iff Module.mem_annihilator
span_singleton_annIdealGenerator 📖	mathematical	—	Ideal.span Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semiring Set Set.instSingletonSet annIdealGenerator annIdeal Semifield.toCommSemiring Ring.toSemiring	—	annIdealGenerator_eq_zero_iff Set.singleton_zero Ideal.span_zero annIdealGenerator.eq_1 Ideal.span_singleton_mul_right_unit isUnit_C Iff.not inv_eq_zero leadingCoeff_eq_zero mul_ne_zero_iff instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain Ideal.span_singleton_generator

---

← Back to Index