mathlib3
df5e9937 - chore(algebra/group_with_zero/units/basic): Deduplicate instance (#18785)

Commit
2 years ago
chore(algebra/group_with_zero/units/basic): Deduplicate instance (#18785) `group_with_zero.cancel_monoid_with_zero` was a duplicate of `group_with_zero.to_cancel_monoid_with_zero`. `comm_group_with_zero.cancel_comm_monoid_with_zero` is renamed to include the usual `to_` prefix. This should have been done in #18698.
Author
Parents
Loading