English
If F has a NonUnitalAlgSemiHomClass structure, then it also carries a NonUnitalRingHomClass structure; i.e., algebra-semihomomorphisms are automatically nonunital ring homomorphisms.
Русский
Если F имеет структуру NonUnitalAlgSemiHomClass, то она автоматически имеет структуру NonUnitalRingHomClass; т.е. алгебро-полу-гомоморфизмы автоматически образуют неунилатные кольцевые гомоморфизмы.
LaTeX
$$$ \\text{NonUnitalAlgSemiHomClass } F φ A B \\Rightarrow \\text{NonUnitalRingHomClass } F A B $$$
Lean4
instance (priority := 100) toNonUnitalRingHomClass {F R S A B : Type*} {_ : Monoid R} {_ : Monoid S}
{φ : outParam (R →* S)} {_ : NonUnitalNonAssocSemiring A} [DistribMulAction R A] {_ : NonUnitalNonAssocSemiring B}
[DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] : NonUnitalRingHomClass F A B :=
{ ‹NonUnitalAlgSemiHomClass F φ A B› with }
