Commit 2025-03-26 11:53 75e44dad

View on Github →

feat(RingTheory): support of quotient module (#20292)

Estimated changes

Modified Mathlib/RingTheory/Localization/Finiteness.lean

Modified Mathlib/RingTheory/Support.lean

modified theorem LocalizedModule.exists_subsingleton_away

modified theorem Module.mem_support_iff_of_finite

modified theorem Module.support_eq_zeroLocus

added theorem Module.support_quotient