val_of

Mathlib.RingTheory.Extension.Basic

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

English

The value of the 'of w' cotangent element is w.

Русский

Значение элемента котангента вида of w равно w.

LaTeX

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

Lean4

@[simp]
theorem val_of : (of w).val = w :=
  rfl

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

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

Разделы

Аффилиация

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