Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-02 14:44 0aa6aed9

View on Github →

chore(order/basic): move strict_mono_coeto subtype NS (#4870) Also add subtype.mono_coe

Estimated changes

Modified src/order/basic.lean

deleted theorem strict_mono_coe

added theorem subtype.mono_coe

added theorem subtype.strict_mono_coe

Modified src/order/conditionally_complete_lattice.lean