Commit 2020-12-05 20:21 1f648141

View on Github →

chore(data/equiv/ring): add symm_symm and coe_symm_mk (#5227) Also generalize map_mul and map_add to [has_mul R] [has_add R] instead of [semiring R].

Estimated changes

Modified src/data/equiv/ring.lean

added theorem ring_equiv.coe_symm_mk

modified theorem ring_equiv.map_add

modified theorem ring_equiv.map_mul

added theorem ring_equiv.symm_symm