mathlib
902b01d8 - chore(algebra/group): rename `is_unit_unit` to `units.is_unit` (#6886)

Commit

4 years ago

chore(algebra/group): rename `is_unit_unit` to `units.is_unit` (#6886)

Author

urkud

urkud

Parents

Loading