mathlib
7aa431c9 - chore(group_theory/quotient_group): Tag lemmas with `@[to_additive]` (#9771)

Commit

4 years ago

chore(group_theory/quotient_group): Tag lemmas with `@[to_additive]` (#9771) Adds `@[to_additive]` to a couple lemmas.

Author

tb65536

Parents