Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-21 16:21 ca554bee

View on Github →

chore(group_theory/quotient_group): make pow definitionally equal (#10833) Motivated by a TODO comment.

Estimated changes

Modified src/group_theory/congruence.lean

Modified src/group_theory/quotient_group.lean

modified theorem quotient_group.coe_div

modified theorem quotient_group.coe_pow

modified theorem quotient_group.coe_zpow