mathlib
0aa6aed9 - chore(order/basic): move `strict_mono_coe`to `subtype` NS (#4870)

Commit

5 years ago

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

References

Author

urkud

Parents