Commit 2022-09-19 03:33 08899973

View on Github →

feat(group_theory/coset): Add quotient_equiv_of_eq (#16439) This PR adds quotient_equiv_of_eq and renames equiv_quotient_of_eq to quotient_mul_equiv_of_eq.

Estimated changes

Modified src/data/zmod/quotient.lean

Modified src/group_theory/coset.lean

added def subgroup.quotient_equiv_of_eq

added theorem subgroup.quotient_equiv_of_eq_mk

Modified src/group_theory/quotient_group.lean

deleted def quotient_group.equiv_quotient_of_eq

deleted theorem quotient_group.equiv_quotient_of_eq_mk

added def quotient_group.quotient_mul_equiv_of_eq

added theorem quotient_group.quotient_mul_equiv_of_eq_mk

Modified src/ring_theory/valuation/valuation_subring.lean