val_add

Mathlib.RingTheory.Extension.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.Cotangent.val_add

English

The value map on cotangent space is additive: val of a sum is the sum of vals.

Русский

Отображение значений на котангентовом пространстве сохраняет сложение: val(x+y) = val(x) + val(y).

LaTeX

$$$\forall x,y \in P.Cotangent,\ (x + y).val = x.val + y.val$$$

Lean4

@[simp]
theorem val_add : (x + y).val = x.val + y.val :=
  rfl

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

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

Разделы

Аффилиация

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