Commit 2025-05-13 12:15 b9ded787

View on Github →

chore: cleanups following #23778 (#24827)

Estimated changes

Modified Mathlib/Algebra/Module/SpanRank.lean

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

modified theorem Ideal.exists_finset_card_eq_height_of_isNoetherianRing

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.exists_subset_radical_span_sup_of_subset_radical_sup

deleted theorem Ideal.exists_subset_radical_span_sup_span_of_subset_radical_sup