addCommGroup — Mathlib

English

The composition distributes over addition: (h ∘ (f + g)) = (h ∘ f) + (h ∘ g).

Русский

Композиция распределяется по сложению: h ∘ (f + g) = (h ∘ f) + (h ∘ g).

LaTeX

$$ (h.comp (f + g)) = h.comp f + h.comp g$$

Lean4

/-- The type of linear maps is an additive group. -/
instance addCommGroup : AddCommGroup (M →ₛₗ[σ₁₂] N₂) :=
  DFunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) fun _ _ ↦ rfl

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