val_zero

Mathlib.RingTheory.Extension.Cotangent.Basic

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

English

For f,g : P.Hom P' and r ∈ S, x ∈ P.Ring, f.sub g(r ⊗ D x) = r • Cotangent.mk (f.subToKer g x).

Русский

Для отображений f,g: P.Hom P' и элементов r ∈ S, x ∈ P.Ring: f.sub g(r ⊗ D x) = r • Cotangent.mk (f.subToKer g x).

LaTeX

$$$f.sub\\ g\\ (r \\otimes_D x) = r \\cdot \\mathrm{Cotangent.mk}(f.subToKer\\ g\\ x)$$$

Lean4

@[simp]
theorem val_zero : (0 : P.H1Cotangent).1 = 0 :=
  rfl

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

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

Разделы

Аффилиация

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