of_add

Mathlib.RingTheory.Extension.Basic

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

English

The map of addition on the kernel-side cotangent is compatible with addition.

Русский

Отображение сложения на котангентах ядра совместимо со сложением.

LaTeX

$$$$\operatorname{of}(w + z) = \operatorname{of}(w) + \operatorname{of}(z)\; (w,z \in P.ker.Cotangent)$$$$

Lean4

@[simp]
theorem of_add : of (w + z) = of w + of z :=
  rfl

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

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

Разделы

Аффилиация

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