Commit 2026-01-18 12:21 cff4d0e1

View on Github →

feat(RingTheory/Ideal/Colon): add a few API lemmas (#34060) This PR adds a few missing API lemmas to RingTheory/Ideal/Colon.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Colon.lean

added theorem Submodule.colon_bot

added theorem Submodule.colon_finsetInf

added theorem Submodule.colon_singleton_zero

added theorem Submodule.mem_colon_iff_le