ring): add `symm_symm` and `coe_symm_mk` (#5227)

Commit

5 years ago

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

Author

urkud

Parents

d4bd4cda

mathlib 1f648141 - chore(data/equiv/ring): add `symm_symm` and `coe_symm_mk` (#5227)

mathlib
1f648141 - chore(data/equiv/ring): add `symm_symm` and `coe_symm_mk` (#5227)