instSub — Mathlib

English

The subtraction of two linear maps is linear: f - g ∈ M →ₛₗ[σ₁₂] N₂.

Русский

Вычитание двух линейных отображений линейно: f - g ∈ M →ₛₗ[σ₁₂] N₂.

LaTeX

$$Sub (M →ₛₗ[σ₁₂] N₂)$$

Lean4

/-- The subtraction of two linear maps is linear. -/
instance : Sub (M →ₛₗ[σ₁₂] N₂) :=
  ⟨fun f g ↦
    { toFun := f - g
      map_add' := fun x y ↦ by simp only [Pi.sub_apply, map_add, add_sub_add_comm]
      map_smul' := fun r x ↦ by simp [Pi.sub_apply, smul_sub] }⟩

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