English
LinearMapClass F R M M₂ is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂; i.e., F is a class of R-linear maps M → M₂.
Русский
LinearMapClass F R M M₂ обозначает класс F как множество R-линейных отображений M → M₂; то есть это синоним SemilinearMapClass F (RingHom.id R) M M₂.
LaTeX
$$$\text{LinearMapClass } F R M M_2 \equiv \text{SemilinearMapClass } F (RingHom.id R) M M_2$$$
Lean4
/-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`.
This is an abbreviation for `SemilinearMapClass F (RingHom.id R) M M₂`.
-/
abbrev LinearMapClass (F : Type*) (R : outParam Type*) (M M₂ : Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂]
[Module R M] [Module R M₂] [FunLike F M M₂] :=
SemilinearMapClass F (RingHom.id R) M M₂
