mathlib
08899973 - feat(group_theory/coset): Add `quotient_equiv_of_eq` (#16439)

Commit
3 years ago
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`.
Author
Parents
Loading