ContentIdeal

📁 Source: Mathlib/RingTheory/Polynomial/ContentIdeal.lean

Statistics

Metric	Count
Definitions contentIdeal	1
Theorems coeff_mem_contentIdeal, contentIdeal_C, contentIdeal_FG, contentIdeal_def, contentIdeal_eq_bot_iff, contentIdeal_eq_top_of_contentIdeal_mul_eq_top, contentIdeal_le_contentIdeal_of_dvd, contentIdeal_le_span_content, contentIdeal_map_eq_map_contentIdeal, contentIdeal_monomial, contentIdeal_mul_eq_top_of_contentIdeal_eq_top, contentIdeal_mul_le_mul_contentIdeal, contentIdeal_one, contentIdeal_zero, isPrimitive_iff_contentIdeal_eq_top, isPrimitive_of_contentIdeal_eq_top, mul_contentIdeal_le_radical_contentIdeal_mul, contentIdeal_eq_span_content_of_isPrincipal, contentIdeal_generator_dvd, contentIdeal_generator_dvd_coeff, contentIdeal_le_span_iff_dvd, isPrimitive_iff_contentIdeal_eq_top	22
Total	23

Polynomial

Definitions

Name	Category	Theorems
contentIdeal 📖	CompOp	21 math math: contentIdeal_one, contentIdeal_def, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, isPrimitive_iff_contentIdeal_eq_top, Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff, contentIdeal_eq_top_iff_forall_gaussNorm_eq_one, gaussNorm_lt_one_iff_contentIdeal_le, Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal, contentIdeal_C, contentIdeal_FG, contentIdeal_map_eq_map_contentIdeal, contentIdeal_monomial, contentIdeal_eq_bot_iff, contentIdeal_zero, Submodule.IsPrincipal.contentIdeal_generator_dvd, contentIdeal_le_span_content, contentIdeal_mul_le_mul_contentIdeal, contentIdeal_le_contentIdeal_of_dvd, mul_contentIdeal_le_radical_contentIdeal_mul, coeff_mem_contentIdeal, Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_mem_contentIdeal 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule contentIdeal coeff	—	AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Ideal.subset_span coeff_mem_coeffs
contentIdeal_C 📖	mathematical	—	contentIdeal DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Ideal.span Set Set.instSingletonSet	—	monomial_zero_left contentIdeal_monomial
contentIdeal_FG 📖	mathematical	—	Ideal.FG contentIdeal	—	—
contentIdeal_def 📖	mathematical	—	contentIdeal Ideal.span SetLike.coe Finset Finset.instSetLike coeffs	—	—
contentIdeal_eq_bot_iff 📖	mathematical	—	contentIdeal Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial instZero	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq coeff_mem_coeffs leadingCoeff_ne_zero Finset.coe_empty instIsEmptyFalse
contentIdeal_eq_top_of_contentIdeal_mul_eq_top 📖	—	contentIdeal CommSemiring.toSemiring Polynomial instMul Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—	le_antisymm le_top IsScalarTower.right contentIdeal_mul_le_mul_contentIdeal Ideal.mul_le_right Ideal.instIsTwoSided
contentIdeal_le_contentIdeal_of_dvd 📖	mathematical	Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule contentIdeal	—	le_trans IsScalarTower.left contentIdeal_mul_le_mul_contentIdeal Ideal.mul_le_right Ideal.instIsTwoSided
contentIdeal_le_span_content 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule contentIdeal Ideal.span Set Set.instSingletonSet content	—	contentIdeal_def Ideal.span_le mem_coeffs_iff Finset.mem_coe SetLike.mem_coe Ideal.mem_span_singleton content_dvd_coeff
contentIdeal_map_eq_map_contentIdeal 📖	mathematical	—	contentIdeal map Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Set.ext Set.union_singleton coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.map_span Ideal.span_insert_zero
contentIdeal_monomial 📖	mathematical	—	contentIdeal DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial Ideal.span Set Set.instSingletonSet	—	monomial_zero_right Finset.coe_empty Ideal.span_empty Ideal.span_zero coeffs_monomial Finset.coe_singleton
contentIdeal_mul_eq_top_of_contentIdeal_eq_top 📖	mathematical	contentIdeal CommSemiring.toSemiring CommRing.toCommSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Polynomial instMul	—	Ideal.radical_eq_top le_antisymm le_top IsScalarTower.right Ideal.mul_top Ideal.instIsTwoSided_1 mul_contentIdeal_le_radical_contentIdeal_mul
contentIdeal_mul_le_mul_contentIdeal 📖	mathematical	—	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule contentIdeal Polynomial instMul Submodule.mul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left contentIdeal_def Ideal.span_le coeff_mul Submodule.addSubmonoidClass
contentIdeal_one 📖	mathematical	—	contentIdeal Polynomial instOne Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.span_singleton_one contentIdeal_C C_1
contentIdeal_zero 📖	mathematical	—	contentIdeal Polynomial instZero Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Finset.coe_empty Ideal.span_empty
isPrimitive_iff_contentIdeal_eq_top 📖	mathematical	—	IsPrimitive contentIdeal CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top IsBezout.isPrincipal_of_FG contentIdeal_FG
isPrimitive_of_contentIdeal_eq_top 📖	mathematical	contentIdeal CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	IsPrimitive	—	top_isPrincipal Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd
mul_contentIdeal_le_radical_contentIdeal_mul 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.right Algebra.id contentIdeal Ideal.radical Polynomial instMul	—	IsScalarTower.right Ideal.radical_eq_sInf le_sInf_iff Ideal.IsPrime.mul_le Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.mk_ker map_mul instNoZeroDivisors Ideal.Quotient.noZeroDivisors

Submodule.IsPrincipal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contentIdeal_eq_span_content_of_isPrincipal 📖	mathematical	—	Polynomial.contentIdeal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet Polynomial.content	—	le_antisymm Polynomial.contentIdeal_le_span_content Ideal.span_singleton_generator Ideal.span_singleton_le_span_singleton Polynomial.content.eq_1 Finset.dvd_gcd_iff contentIdeal_generator_dvd_coeff
contentIdeal_generator_dvd 📖	mathematical	—	Polynomial CommSemiring.toSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C generator NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.contentIdeal	—	Polynomial.C_dvd_iff_dvd_coeff contentIdeal_generator_dvd_coeff
contentIdeal_generator_dvd_coeff 📖	mathematical	—	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring generator CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.contentIdeal Polynomial.coeff	—	Polynomial.coeff_mem_contentIdeal mem_iff_eq_smul_generator
contentIdeal_le_span_iff_dvd 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.contentIdeal Ideal.span Set Set.instSingletonSet Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring DFunLike.coe RingHom Polynomial.semiring RingHom.instFunLike Polynomial.C	—	Ideal.span_singleton_generator instIsTransDvd map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Ideal.span_singleton_le_span_singleton contentIdeal_generator_dvd Polynomial.contentIdeal_C Polynomial.contentIdeal_le_contentIdeal_of_dvd
isPrimitive_iff_contentIdeal_eq_top 📖	mathematical	—	Polynomial.IsPrimitive Polynomial.contentIdeal CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Mathlib.Tactic.Contrapose.contrapose₁ contentIdeal_generator_dvd Ideal.span_singleton_generator Polynomial.isPrimitive_of_contentIdeal_eq_top

---

← Back to Index