Lasker

📁 Source: Mathlib/RingTheory/Lasker.lean

Statistics

Metric	Count
Definitions IsMinimalPrimaryDecomposition, IsLasker, IsMinimalPrimaryDecomposition	3
Theorems exists_isMinimalPrimaryDecomposition, minimal, minimalPrimes_subset_image_radical, decomposition_erase_inf, exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, isLasker, isPrimary_decomposition_pairwise_ne_radical, isPrimary, exists_isMinimalPrimaryDecomposition, distinct, inf_eq, minimal, primary, decomposition_erase_inf, exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, isLasker, isPrimary_decomposition_pairwise_ne_radical	17
Total	20

Ideal

Definitions

Name	Category	Theorems
IsMinimalPrimaryDecomposition 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decomposition_erase_inf 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instOrderTop	Finset Finset.instHasSubset Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Finset.erase	—	Submodule.decomposition_erase_inf
exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instOrderTop Submodule.IsPrimary	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Ideal radical Submodule.colon Set.univ Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Finset.erase	—	Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition
isLasker 📖	mathematical	—	IsLasker CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Submodule.isLasker
isPrimary_decomposition_pairwise_ne_radical 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instOrderTop Submodule.IsPrimary	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Ideal radical Submodule.colon Set.univ	—	Submodule.isPrimary_decomposition_pairwise_ne_radical

Ideal.IsLasker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isMinimalPrimaryDecomposition 📖	mathematical	IsLasker	Submodule.IsMinimalPrimaryDecomposition	—	Submodule.IsLasker.exists_isMinimalPrimaryDecomposition
minimal 📖	mathematical	IsLasker	Submodule.IsMinimalPrimaryDecomposition	—	Submodule.IsLasker.exists_isMinimalPrimaryDecomposition

Ideal.IsMinimalPrimaryDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minimalPrimes_subset_image_radical 📖	mathematical	Submodule.IsMinimalPrimaryDecomposition NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	Set Ideal Set.instHasSubset Ideal.minimalPrimes Set.image Ideal.radical SetLike.coe Finset Finset.instSetLike	—	Ideal.IsPrime.radical le_trans Submodule.IsMinimalPrimaryDecomposition.inf_eq Ideal.radicalInfTopHom_apply map_finset_inf InfTopHom.instInfTopHomClass le_refl Ideal.radical_mono Ideal.IsPrime.inf_le' le_antisymm Ideal.isPrime_radical Submodule.IsMinimalPrimaryDecomposition.primary Eq.trans_le LE.le.trans Finset.inf_le Ideal.le_radical

InfIrred

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrimary 📖	mathematical	InfIrred Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	Submodule.IsPrimary	—	Submodule.IsPrimary.eq_1 ne_top smul_add Submodule.add_mem smul_zero AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass SMulCommClass.smul_comm smulCommClass_self Submodule.smul_mem smul_smul monotone_stabilizes_iff_noetherian pow_succ SemigroupAction.mul_smul sup_eq_left Submodule.add_eq_sup le_antisymm le_add_self Nat.instCanonicallyOrderedAdd Submodule.add_mem_iff_right pow_add le_inf

Submodule

Definitions

Name	Category	Theorems
IsMinimalPrimaryDecomposition 📖	CompData	3 math math: Ideal.IsLasker.minimal, Ideal.IsLasker.exists_isMinimalPrimaryDecomposition, IsLasker.exists_isMinimalPrimaryDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decomposition_erase_inf 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instOrderTop	Finset Finset.instHasSubset Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.erase	—	Finset.eraseInduction Finset.Subset.rfl Mathlib.Tactic.Push.not_forall_eq HasSubset.Subset.trans Finset.instIsTransSubset Finset.erase_subset Finset.insert_erase Finset.inf_insert inf_of_le_right
exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instOrderTop IsPrimary	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Ideal Ideal.radical colon Set.univ Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.erase	—	isPrimary_decomposition_pairwise_ne_radical decomposition_erase_inf Set.Pairwise.mono
isLasker 📖	mathematical	—	IsLasker CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	InfIrred.isPrimary exists_infIrred_decomposition wellFoundedGT
isPrimary_decomposition_pairwise_ne_radical 📖	mathematical	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instOrderTop IsPrimary	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Ideal Ideal.radical colon Set.univ	—	ext isPrimary_finsetInf Finset.coe_image Mathlib.Tactic.Contrapose.contrapose₄ Ideal.radical_finset_inf colon_finsetInf

Submodule.IsLasker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isMinimalPrimaryDecomposition 📖	mathematical	IsLasker	Submodule.IsMinimalPrimaryDecomposition	—	Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

Submodule.IsMinimalPrimaryDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distinct 📖	mathematical	Submodule.IsMinimalPrimaryDecomposition	Set.Pairwise Submodule CommSemiring.toSemiring SetLike.coe Finset Finset.instSetLike Function.onFun Ideal Ideal.radical Submodule.colon Set.univ	—	—
inf_eq 📖	mathematical	Submodule.IsMinimalPrimaryDecomposition	Finset.inf Submodule CommSemiring.toSemiring Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instOrderTop	—	—
minimal 📖	mathematical	Submodule.IsMinimalPrimaryDecomposition Submodule CommSemiring.toSemiring Finset Finset.instMembership	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Finset.inf Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.instOrderTop Finset.erase	—	—
primary 📖	mathematical	Submodule.IsMinimalPrimaryDecomposition Submodule CommSemiring.toSemiring Finset Finset.instMembership	Submodule.IsPrimary	—	—

(root)

Definitions

Name	Category	Theorems
IsLasker 📖	MathDef	2 math math: Ideal.isLasker, Submodule.isLasker

---

← Back to Index