coe_add' — Mathlib

English

For a finite index set ι and f_i ∈ End_R(M1,M2), the sum ∑_{i∈t} f_i is again an endomorphism, and its action is the sum of the actions: (∑ f_i)(x) = ∑ f_i(x).

Русский

Для конечного множества индексов ι и эндоморфизмов f_i ∈ End_R(M1,M2) сумма ∑_{i∈t} f_i снова является эндоморфизмом и действует по правилу (∑ f_i)(x) = ∑ f_i(x).

LaTeX

$$$\\forall t \\subseteq ι\\; (f_i)_{i∈t}: \\; (\\sum_{i\\in t} f_i)(x) = \\sum_{i\\in t} f_i(x).$$$

Lean4

@[norm_cast]
theorem coe_add' (f g : M₁ →SL[σ₁₂] M₂) : ⇑(f + g) = f + g :=
  rfl

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