linearCombination_zero_apply

Mathlib.LinearAlgebra.Finsupp.LinearCombination

URI: https://scilib.ai/kg/mathlib#Finsupp.linearCombination_zero_apply

English

For x ∈ α →₀ R, (linearCombination_R(0))(x) = 0.

Русский

Для любого $x$ из $(\alpha \to_R M)$ выполняется $(\operatorname{linearCombination}_R(0))(x) = 0$.

LaTeX

$$$\operatorname{linearCombination}_R(0)(x) = 0.$$$

Lean4

theorem linearCombination_zero_apply (x : α →₀ R) : (linearCombination R (0 : α → M)) x = 0 := by
  simp [linearCombination_apply]

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

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

Разделы

Аффилиация

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