units): better defeq for is_unit.unit (#9112)

Commit

4 years ago

refactor(algebra/group/units): better defeq for is_unit.unit (#9112) Make sure that, for `x : M` and `h : is_unit M`, then `is_unit.unit x h : M` is defeq to `x`.

Author

sgouezel

Parents

574864d3

mathlib3 92e7bbe9 - refactor(algebra/group/units): better defeq for is_unit.unit (#9112)

mathlib3
92e7bbe9 - refactor(algebra/group/units): better defeq for is_unit.unit (#9112)