English
A class of maps preserving additively and commuting with the action is a structured morphism class compatible with the scalar actions.
Русский
Класс отображений, сохраняющих сложение и совместимый с действиями скаляр, является согласованным классом морфизмов.
LaTeX
$$$\text{DistribMulActionHomClass } F M A B$ is a Prop describing morphisms preserving addition and commuting with the $M$-action.$$
Lean4
/-- `DistribMulActionHomClass F M A B` states that `F` is a type of morphisms preserving
the additive monoid structure and equivariant with respect to the action of `M`.
It is an abbreviation to `DistribMulActionHomClass F (MonoidHom.id M) A B`
You should extend this class when you extend `DistribMulActionHom`. -/
abbrev DistribMulActionHomClass (F : Type*) (M : outParam Type*) (A B : outParam Type*) [Monoid M] [AddMonoid A]
[AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] :=
DistribMulActionSemiHomClass F (MonoidHom.id M) A B
