δ_eq_δ

Mathlib.RingTheory.Kaehler.JacobiZariski

URI: https://scilib.ai/kg/mathlib#Algebra.Generators.H1Cotangent.δ_eq_δ

English

δ is independent of choice of P and P' for all generators; δ Q P = δ Q P'.

Русский

δ не зависит от выбора P и P' для любых порождающих; δ Q P = δ Q P'.

LaTeX

$$$δ Q P = δ Q P'$$$

Lean4

theorem δ_eq_δ : δ Q P = δ Q P' := by
  ext ⟨x, hx⟩
  obtain ⟨x, rfl⟩ := Extension.Cotangent.mk_surjective x
  rw [δ_eq_δAux, δ_eq_δAux]

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

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

Разделы

Аффилиация

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