val_add

Mathlib.RingTheory.Extension.Cotangent.Basic

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

English

There is a canonical Module structure on H1Cotangent given by δ, compatible with the IsScalarTower framework.

Русский

Существует каноническая структура модуля на H1Cotangent, заданная через δ, совместимая с рамкой IsScalarTower.

LaTeX

$$$\\text{instance: } H1Cotangent \\; \\text{is a module over } R$$$

Lean4

@[simp]
theorem val_add (x y : P.H1Cotangent) : (x + y).1 = x.1 + y.1 :=
  rfl

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

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

Разделы

Аффилиация

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