Commit 2024-10-28 20:27 d131995e

View on Github →

feat(RingTheory/IsLasker): strength primary decomposition to a minimal one (#18296) Each primary ideal in the decomposition is necessary, and has an indepedent radical.

Estimated changes

Modified Mathlib/Data/Finset/Lattice.lean

added theorem Finset.inf'_eq_of_forall

added theorem Finset.sup'_eq_of_forall

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

added theorem Ideal.isPrimary_finset_inf

Modified Mathlib/RingTheory/Ideal/Operations.lean

added def Ideal.radicalInfTopHom

added theorem Ideal.radicalInfTopHom_apply

added theorem Ideal.radical_finset_inf

Modified Mathlib/RingTheory/Lasker.lean

added theorem Ideal.IsLasker.minimal

added theorem Ideal.decomposition_erase_inf

deleted theorem Ideal.exists_isPrimary_decomposition

added theorem Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

modified theorem Ideal.isLasker

added theorem Ideal.isPrimary_decomposition_pairwise_ne_radical