of_val

Mathlib.RingTheory.Extension.Basic

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

English

Applying of to a cotangent element and then taking its val yields the original element in the kernel.

Русский

Применение of к котангентовскому элементу и взятие его значения восстанавливает исходный элемент ядра.

LaTeX

$$$$ (\mathrm{of}\, w).\mathrm{val} = w \quad (w \in P.ker.Cotangent)$$$$

Lean4

@[simp]
theorem of_val : of x.val = x :=
  rfl

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

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

Разделы

Аффилиация

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