mathlib
0d17cfb6 - chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821)

Commit

3 years ago

chore(group_theory/quotient_group): drop unneeded names in `to_additive` (#17821) This only changes the names of `group` and `comm_group` instances.

Author

urkud

Parents