Commit 2026-09-09 08:54 62d0e074
View on Github →chore: rename Alg{Hom,Equiv}Class.toAlg{Hom,Equiv} to Alg{Hom,Equiv}.ofClass (#43557) and rename affected lemmas accordingly. Following item (2) in https://github.com/leanprover-community/mathlib4/issues/31365, the definition which implements the coercion from a morphism class FooHomClass to FooHoms should be called FooHom.ofClass. This makes two more classes follow this pattern.