English
NonUnitalAlgHomClass F R A B is defined as an abbreviation of NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B; i.e., it is a specialization with the identity ring hom.
Русский
NonUnitalAlgHomClass F R A B задаётся как сокращение от NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B; то есть это специализация с тождественным гомоморфизмом R.
LaTeX
$$$ \\text{NonUnitalAlgHomClass}(F,R,A,B) \\equiv \\text{NonUnitalAlgSemiHomClass}(F,\\mathrm{MonoidHom.id}\,R,A,B) $$$
Lean4
/-- `NonUnitalAlgHomClass F R A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B` which are `R`-linear.
This is an abbreviation to `NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B` -/
abbrev NonUnitalAlgHomClass (F : Type*) (R A B : outParam Type*) [Monoid R] [NonUnitalNonAssocSemiring A]
[NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] :=
NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B
