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]
.
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]
.