English
There is an additive action of the partial linear maps on themselves given by vadd, with zero acting as the identity and associativity compatible with map addition.
Русский
Существует добавочное действие частичных линейных отображений на их самом множестве, заданное через vadd, при этом нулевой элемент действует как тождественный, а ассоциативность совместима с обычным сложением отображений.
LaTeX
$$$$ \\text{There exists an AddAction on } \\mathrm{LinearPMap}(R,E,F) \\text{ with } \\mathrm{vadd} := (\\cdot +_{\\mathrm{v}} \\cdot),\\; 0_{\\mathrm{v}}(x)=x,\\; (f_1+_{\\mathrm{v}} f_2)\\;\\text{is compatible with } f_1+f_2. $$$$
Lean4
instance instAddAction : AddAction (E →ₗ[R] F) (E →ₗ.[R] F)
where
vadd := (· +ᵥ ·)
zero_vadd := fun ⟨_s, _f⟩ => ext' <| zero_add _
add_vadd := fun _f₁ _f₂ ⟨_s, _g⟩ => ext' <| LinearMap.ext fun _x => add_assoc _ _ _
