mathlib
ea665e7d - fix(algebra/ordered*): add norm_cast attribute (#3132)

Commit

5 years ago

fix(algebra/ordered*): add norm_cast attribute (#3132) Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author

kbuzzard

Parents