Commit 2023-03-02 18:05 27b54c47
View on Github →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