mathlib

4ea65cad - chore(algebra/algebra/basic): missing lemmas about the `↑` spelling of `algebra_map` (#18422)

chore(algebra/algebra/basic): missing lemmas about the `↑` spelling of `algebra_map` (#18422) This only really scratches the surface; in general we can't afford to have two different spellings here as it forces us to duplicate every result about `ring_hom`. A previously refactor (#17048) made these lemmas unecessary, but it was reverted to aid with the port. Since these lemmas are needed in mathlib3 PRs, lets have them anyway. For consistency with the existing `algebra_map.coe_mul` etc, these are not `simp` lemmas. Making them `simp` lemmas makes a bunch of downstream `simp` lemmas redundant; so perhaps worth exploring in a future PR.