mathlib

b6c8c0d4 - refactor(linear_algebra/quotient): Use the same quotient relation as add_subgroup (#13620)

refactor(linear_algebra/quotient): Use the same quotient relation as add_subgroup (#13620) This means that the quotient by `p` and `p.to_add_subgroup` are defeq as types, and the instances defined on them are defeq too. This removes a TODO comment by Mario; I can only assume it resolves it in the right direction