Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 301542a4

View on Github →

feat(group_theory.quotient_group): add eq_iff_div_mem (#7523) From LTE. Written by @PatrickMassot

Estimated changes

Modified src/group_theory/quotient_group.lean

added theorem quotient_group.eq_iff_div_mem

added theorem quotient_group.eq_one_iff

Modified src/group_theory/subgroup.lean

added theorem subgroup.exists_inv_mem_iff_exists_mem