mathlib3

27b54c47 - fix(algebra/algebra/operations): add missing `set_semiring.down` casts (#18539)

fix(algebra/algebra/operations): add missing `set_semiring.down` casts (#18539) Previously this was abusing the defeq of the types, resulting in lemmas stated in weird ways. This also fixes a type in #18449, and adds three missing lemmas about `image_hom`. Forward port of `set_semiring` will be included in https://github.com/leanprover-community/mathlib4/pull/2518