coe_sum

Mathlib.Algebra.Algebra.Basic

URI: https://scilib.ai/kg/mathlib#algebraMap.coe_sum

English

The sum is preserved by the algebra map: the image of a sum equals the sum of images.

Русский

Сумма сохраняется отображением алгебраMap: образ суммы равен сумме образов.

LaTeX

$$$\\big(\\sum_{i\\in s} a_i\\big)^{A} = \\sum_{i\\in s} (a_i)^{A}$$$

Lean4

@[norm_cast]
theorem coe_sum (a : ι → R) : ↑(∑ i ∈ s, a i) = ∑ i ∈ s, (↑(a i) : A) :=
  map_sum (algebraMap R A) a s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru