Commit 2025-06-23 17:18 c31e1e19

View on Github →

refactor(RingTheory/Ideal/Colon): generalize Ideal.mem_colon_singleton (#25850) This PR generalizes a bit the assumptions of Ideal.mem_colon_singleton, changing CommRing R and AddCommGroup M to CommSemiring R and AddCommMonoid R. It also removes some unused variables from Mathlib/RingTheory/Ideal/Colon.lean.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Colon.lean

modified theorem Submodule.annihilator_quotient

modified theorem Submodule.mem_colon_singleton