mathlib3
733aed57 - chore(group_theory/index): Add `to_additive` (#13191)

Commit

3 years ago

chore(group_theory/index): Add `to_additive` (#13191) This PR adds `to_additive` to the rest of `group_theory/index.lean`.

Author

tb65536

Parents