Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
strict_mono_coe
Modification history
2020-11-02 14:44
src/order/basic.lean
chore(order/basic): move `strict_mono_coe`to `subtype` NS (#4870) …
Deleted
strict_mono_coe
View on Github →
2020-09-09 13:02
src/order/basic.lean
feat(order/conditionally_complete_lattice, topology/algebra/ordered): inherited order properties for `ord_connected` subset (#3991) …
Added
strict_mono_coe
View on Github →