instAdd — Mathlib

English

The sum of two σ₁₂-linear maps M →ₛₗ[σ₁₂] M₂ is again σ₁₂-linear.

Русский

Сумма двух σ₁₂-линейных отображений из M в M₂ снова линейна по связке σ₁₂.

LaTeX

$$$(f,g : M \to_{\sigma_{12}} M_2) \Rightarrow (f+g) \in M \to_{\sigma_{12}} M_2$$$

Lean4

/-- The sum of two linear maps is linear. -/
instance : Add (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun f g ↦
    { toFun := f + g
      map_add' := by simp [add_comm, add_left_comm]
      map_smul' := by simp [smul_add] }⟩

Похожие утверждения