coeFn_sum — Mathlib

English

The coercion to functions commutes with finite sums: the function underlying sum of a finite family equals the sum of the underlying functions.

Русский

Коэрцировка в функции commute с конечной суммой: функция суммы семейства равна сумме функций.

LaTeX

$$$\\big( \\sum_{i\\in s} Q_i \\big)^{\\text{coe}} = \\sum_{i\\in s} Q_i^{\\text{coe}}$ for a finite set s.$$

Lean4

@[simp, norm_cast]
theorem coeFn_sum {ι : Type*} (Q : ι → QuadraticMap R M N) (s : Finset ι) : ⇑(∑ i ∈ s, Q i) = ∑ i ∈ s, ⇑(Q i) :=
  map_sum coeFnAddMonoidHom Q s

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