Commit 2022-10-04 10:22 93354783

View on Github →

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.

Estimated changes

Modified src/algebra/symmetrized.lean

modified def sym_alg.sym

modified theorem sym_alg.sym_bijective

deleted def sym_alg.sym_equiv

modified theorem sym_alg.sym_injective

modified theorem sym_alg.sym_surjective

added theorem sym_alg.sym_symm

modified def sym_alg.unsym

modified theorem sym_alg.unsym_bijective

modified theorem sym_alg.unsym_injective

modified theorem sym_alg.unsym_surjective

added theorem sym_alg.unsym_symm