refactor(RingTheory/Lasker): generalize from Ideal to Submodule

[tb65536]

This PR generalizes the Lasker-Noether theorem from ideals to submodules.

---

• depends on: feat(RingTheory/IsPrimary): generalize isPrimary_inf to submodules #34061

[github-actions]

PR summary cd9e56bcf7

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.IsPrimary	1054	1059	+5 (+0.47%)
Mathlib.RingTheory.Ideal.IsPrimary	1058	1060	+2 (+0.19%)

Import changes for all files

Files	Import difference
3 files Mathlib.NumberTheory.PrimesCongruentOne Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Polynomial.Cyclotomic.Eval	1
199 files Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Order.Ring.StandardPart Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Galois.IsGaloisGroup Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.FieldTheory.NormalizedTrace Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.SeparablyGenerated Mathlib.LinearAlgebra.Span.TensorProduct Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.Niven Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.Padics.HeightOneSpectrum Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.Padics.WithVal Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 Mathlib.RingTheory.Bialgebra.GroupLike Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Coalgebra.GroupLike Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.Discriminant Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.FractionalIdeal.Inverse Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.HopfAlgebra.GroupLike Mathlib.RingTheory.Ideal.AssociatedPrime.Basic Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.IsPrimary Mathlib.RingTheory.Ideal.MinimalPrime.Basic Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Ideal.NatInt Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime.Basic Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.NormalClosure Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.RingHom.Bijective Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Spectrum.Maximal.Localization Mathlib.RingTheory.Spectrum.Maximal.Topology Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC Mathlib.RingTheory.Spectrum.Prime.RingHom Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.DiscreteValuativeRel Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.Algebra.Valued.WithZeroMulInt	2
Mathlib.RingTheory.IsPrimary	5

---

Declarations diff

+ Ideal.IsLasker.exists_isMinimalPrimaryDecomposition
+ Ideal.IsLasker.minimal
+ Ideal.IsMinimalPrimaryDecomposition
+ Ideal.decomposition_erase_inf
+ Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition
+ Ideal.isLasker
+ Ideal.isPrimary_decomposition_pairwise_ne_radical
+ IsPrimary.mem_or_mem
++ IsPrimary.inf
++ isPrimary_finsetInf
- IsLasker.minimal

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(RingTheory/IsPrimary): generalize isPrimary_inf to submodules #34061
  By Dependent Issues (🤖). Happy coding!