Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 03:34 7aa431c9

View on Github →

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

Estimated changes