Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 20:53 0d17cfb6

View on Github →

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

Estimated changes

modified theorem quotient_group.coe_div
modified theorem quotient_group.coe_inv
modified theorem quotient_group.coe_mul
modified theorem quotient_group.coe_one
modified theorem quotient_group.coe_pow
modified theorem quotient_group.coe_zpow
modified theorem quotient_group.ker_lift_mk'
modified theorem quotient_group.ker_lift_mk
modified theorem quotient_group.ker_mk
modified theorem quotient_group.lift_mk'
modified theorem quotient_group.lift_mk
modified theorem quotient_group.map_coe
modified theorem quotient_group.map_mk'