mathlib
fbcd8908 - chore(data/subtype,order/complete_lattice): use `coe` instead of `subtype.val` (#3518)

Commit
6 years ago
chore(data/subtype,order/complete_lattice): use `coe` instead of `subtype.val` (#3518)
Author
Parents
Loading