addCommGroup — Mathlib

English

The space of continuous linear maps M →L[R] M₂ is an additive commutative group under pointwise addition.

Русский

Множество непрерывных линейных отображений M →L[R] M₂ образует коммутативную группу под точечным сложением.

LaTeX

$$$\text{Hom}_{\text{cont}}(M,M_2) = M \to_L[R] M_2 \text{ with } (f+g)(x)=f(x)+g(x).$$$

Lean4

instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂)
    where
  __ := ContinuousLinearMap.addCommMonoid
  neg := (-·)
  sub := (· - ·)
  sub_eq_add_neg _ _ := by ext; apply sub_eq_add_neg
  nsmul := (· • ·)
  zsmul := (· • ·)
  zsmul_zero' f := by ext; simp
  zsmul_succ' n f := by ext; simp [add_smul, add_comm]
  zsmul_neg' n f := by ext; simp [add_smul]
  neg_add_cancel _ := by ext; apply neg_add_cancel

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