Commit 2024-12-31 21:01 7178aee7

View on Github →

chore(RingTheory/Ideal/Colon): generalize to semiring (#18595) Keep the annihilator eq as a lemma for CommRing

Estimated changes

Modified Mathlib/RingTheory/Ideal/Colon.lean

added theorem Submodule.annihilator_map_mkQ_eq_colon

modified def Submodule.colon

modified theorem Submodule.mem_colon