Documentation Verification Report

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`, `comap_localized₀_eq_iInf`, `comap_localized₀_eq_ite`, `distinct`, `image_radical_eq_associated_primes`, `inf_eq`, `injOn`, `mem_associatedPrimes`, `mem_image_radical_colon_iff`, `minimal`, `primary`, `decomposition_erase_inf`, `exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition`, `isLasker`, `isPrimary_decomposition_pairwise_ne_radical`	23
Total	26

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` `Submodule` `CommSemiring.toSemiring` `Finset.instHasSubset` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Finset.erase` `Submodule.decidableEq`	—	`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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderTop` `Submodule.IsPrimary` `Set.Pairwise` `SetLike.coe` `Finset.instSetLike` `Function.onFun` `Ideal` `radical` `Submodule.colon` `Set.univ` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Finset.erase` `Submodule.decidableEq`	—	`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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderTop` `Submodule.IsPrimary` `Set.Pairwise` `SetLike.coe` `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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Submodule.IsMinimalPrimaryDecomposition`	—	`Submodule.IsLasker.exists_isMinimalPrimaryDecomposition`
`minimal` 📖	mathematical	`IsLasker`	`Finset` `Submodule` `CommSemiring.toSemiring` `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` `CommSemiring.toSemiring` `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` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`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` `Submodule` `CommSemiring.toSemiring` `Finset.instHasSubset` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Finset.erase` `decidableEq`	—	`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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderTop` `IsPrimary` `Set.Pairwise` `SetLike.coe` `Finset.instSetLike` `Function.onFun` `Ideal` `Ideal.radical` `colon` `Set.univ` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Finset.erase` `decidableEq`	—	`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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `instOrderTop` `IsPrimary` `Set.Pairwise` `SetLike.coe` `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`	`Finset` `Submodule` `CommSemiring.toSemiring` `Submodule.IsMinimalPrimaryDecomposition`	—	`Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition`

Submodule.IsMinimalPrimaryDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_localized₀_eq_iInf` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition` `CommRing.toCommSemiring` `IsLowerSet` `Set.Elem` `Ideal` `CommSemiring.toSemiring` `Submodule.associatedPrimes` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule` `Finset.instHasSubset` `Finset.image` `Submodule.decidableEq` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.radical` `Submodule.colon` `Set.univ`	`Submodule.comap` `LocalizedModule` `CommRing.toCommSemiring` `iInf` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.Elem` `Ideal` `Submodule.associatedPrimes` `Submonoid.instInfSet` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Ideal.primeCompl` `Set` `Set.instMembership` `Submodule.instIsPrimeValIdealMemSetAssociatedPrimes` `OreLocalization.instAddCommMonoidOreLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Module.toDistribMulAction` `OreLocalization.instModuleOfIsScalarTower` `Semiring.toModule` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `IsScalarTower.right` `Algebra.id` `RingHom.id` `LocalizedModule.mkLinearMap` `Submodule.localized₀` `localizedModuleIsLocalizedModule` `Submodule` `Submodule.instInfSet`	—	`Submodule.instIsPrimeValIdealMemSetAssociatedPrimes` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `inf_eq` `Submodule.IsLocalizedModule.localized₀FrameHom_apply` `map_finset_inf` `FrameHomClass.toInfTopHomClass` `FrameHom.instFrameHomClass` `Submodule.comap_finsetInf` `RingHomSurjective.ids` `mem_associatedPrimes` `comap_localized₀_eq_ite` `primary` `Set.InjOn.mem_image_iff` `injOn` `Finset.inf_congr` `Finset.inf_ite` `Finset.inf_top` `inf_top_eq` `Finset.filter_mem_eq_inter` `Finset.inter_eq_right` `Finset.inf_eq_iInf`
`comap_localized₀_eq_ite` 📖	mathematical	`IsLowerSet` `Set.Elem` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.associatedPrimes` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.IsPrimary` `Ideal.radical` `Submodule.colon` `Set.univ`	`Submodule.comap` `LocalizedModule` `CommRing.toCommSemiring` `iInf` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Set.Elem` `Ideal` `Submodule.associatedPrimes` `Submonoid.instInfSet` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Ideal.primeCompl` `Set` `Set.instMembership` `Submodule.instIsPrimeValIdealMemSetAssociatedPrimes` `OreLocalization.instAddCommMonoidOreLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Module.toDistribMulAction` `OreLocalization.instModuleOfIsScalarTower` `Semiring.toModule` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `IsScalarTower.right` `Algebra.id` `RingHom.id` `LocalizedModule.mkLinearMap` `Submodule.localized₀` `localizedModuleIsLocalizedModule` `Submodule` `Finset.decidableMem` `Submodule.decidableEq` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Top.top` `Submodule.instTop`	—	`Submodule.instIsPrimeValIdealMemSetAssociatedPrimes` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule` `le_antisymm` `IsLocalizedModule.eq_iff_exists` `LinearMap.map_smul_of_tower` `LinearMap.IsScalarTower.compatibleSMul` `Submonoid.isScalarTower` `OreLocalization.instIsScalarTower` `IsLocalizedModule.mk'_eq_iff` `Submodule.smul_mem` `Submodule.IsPrimary.mem_or_mem` `smul_smul` `Submonoid.smul_def` `RingHomSurjective.ids` `Submodule.map_le_iff_le_comap` `Submodule.map_le_localized₀` `Mathlib.Tactic.Contrapose.contrapose₄` `Ideal.subset_union_prime` `Submodule.IsAssociatedPrime.toIsPrime` `Ideal.IsPrime.radical_le_iff` `Set.not_subset_iff_exists_mem_notMem` `Set.mem_biUnion` `eq_top_iff` `Submodule.map_top` `Set.smul_mem_smul_set` `Set.mem_univ`
`distinct` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition`	`Set.Pairwise` `Submodule` `CommSemiring.toSemiring` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Ideal` `Ideal.radical` `Submodule.colon` `Set.univ`	—	—
`image_radical_eq_associated_primes` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition`	`Set.image` `Submodule` `CommSemiring.toSemiring` `Ideal` `Ideal.radical` `Submodule.colon` `Set.univ` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.associatedPrimes`	—	`inf_eq` `Submodule.colon_finsetInf` `map_finset_inf` `InfTopHom.instInfTopHomClass` `Finset.inf_congr` `Submodule.IsPrimary.radical_colon_singleton_eq_ite` `primary` `Finset.inf_ite` `Finset.inf_top` `top_inf_eq` `Set.ext` `SetLike.not_le_iff_exists` `instIsConcreteLE` `minimal` `Submodule.IsPrimary.isPrime_radical_colon` `Finset.insert_erase` `Finset.mem_filter` `Finset.inf_insert` `inf_eq_left` `Finset.le_inf_iff` `Ideal.eq_inf_of_isPrime_inf` `Finset.mem_of_mem_filter`
`inf_eq` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition`	`Finset.inf` `Submodule` `CommSemiring.toSemiring` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderTop`	—	—
`injOn` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition`	`Set.InjOn` `Submodule` `CommSemiring.toSemiring` `Ideal` `Ideal.radical` `Submodule.colon` `Set.univ` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.injOn_iff_pairwise_ne` `distinct`
`mem_associatedPrimes` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition` `Submodule` `CommSemiring.toSemiring` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Submodule.associatedPrimes` `Ideal.radical` `Submodule.colon` `Set.univ`	—	`image_radical_eq_associated_primes` `Set.mem_image_of_mem`
`mem_image_radical_colon_iff` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition`	`Set.image` `Submodule` `CommSemiring.toSemiring` `Ideal` `Ideal.radical` `Submodule.colon` `Set.univ` `SetLike.coe` `Finset` `Finset.instSetLike` `Submodule.associatedPrimes`	—	`image_radical_eq_associated_primes`
`minimal` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition` `Submodule` `CommSemiring.toSemiring` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Submodule` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Finset.inf` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.instOrderTop` `Finset.erase` `Submodule.decidableEq`	—	—
`primary` 📖	mathematical	`Submodule.IsMinimalPrimaryDecomposition` `Submodule` `CommSemiring.toSemiring` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Submodule.IsPrimary`	—	—

(root)

Definitions

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

---

← Back to Index