Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-09 12:20 735a26e5

View on Github →

chore(group_theory): some new convenience lemmas (#7555) from LTE

Estimated changes

Modified src/group_theory/coset.lean

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.coe_mk'

added theorem quotient_group.mk'_apply

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.eq_iff

added theorem subgroup.div_mem_comm_iff

Modified src/topology/algebra/group.lean