restrictScalars_add — Mathlib

English

The restriction map preserves addition of continuous linear maps: (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R.

Русский

Ограничение сохраняет сложение: (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R.

LaTeX

$$$$ (f + g)_{|R} = f_{|R} + g_{|R}. $$$$

Lean4

@[simp]
theorem restrictScalars_add [ContinuousAdd M₂] (f g : M₁ →L[A] M₂) :
    (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R :=
  rfl

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