mathlib3
6365c6c1 - feat(algebra/invertible): construction from is_unit (#8205)

Commit

4 years ago

feat(algebra/invertible): construction from is_unit (#8205) Co-authored-by: Johan Commelin <johan@commelin.net>

Author

eric-wieser

Parents