English
The set of continuous linear endomorphisms End_R(M1,M2) carries the structure of an additive commutative monoid, with zero and addition defined pointwise.
Русский
Множество непрерывных линейных эндоморфизмов End_R(M1,M2) имеет структуру аддитивной коммутативной моноиды: ноль и сложение определены по точкам.
LaTeX
$$$End_R(M_1,M_2) \\text{ is an AddCommMonoid with } (f+g)(x)=f(x)+g(x) \\text{ and } 0(x)=0.$$$
Lean4
instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂)
where
zero_add := by
intros
ext
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
add_zero := by
intros
ext
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
add_comm := by
intros
ext
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
add_assoc := by
intros
ext
apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
nsmul := (· • ·)
nsmul_zero
f := by
ext
simp
nsmul_succ n
f := by
ext
simp [add_smul]
