mathlib

af36f1a3 - chore(algebra/group/ulift): use injective.* to define instances (#10172)

chore(algebra/group/ulift): use injective.* to define instances (#10172) Also rename `ulift.mul_equiv` to `mul_equiv.ulift` and add some missing instances. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>