mathlib3

93354783 - refactor(algebra/symmetrized): Bundle `sym` and `unsym` as equivalences (#14334)

refactor(algebra/symmetrized): Bundle `sym` and `unsym` as equivalences (#14334) Coercions to and from a type synonym should be bundled as (decorated) equivalences to be maximally useful. This PR bundles `sym_alg.sym` and `sym_alg.unsym` that way. As a result, `sym_alg.sym_equiv` is now redundant.