Mathlib Changelog
v4
Changelog
About
Github
Theorem
compRel_right_mono
Modification history
2025-07-31 09:17
Mathlib/Topology/UniformSpace/Defs.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Deleted
compRel_right_mono
View on Github →
2025-06-11 23:54
Mathlib/Topology/UniformSpace/Defs.lean
chore: remove last use of `mono` tactic (#25698) …
Added
compRel_right_mono
View on Github →