liftKaehlerDifferential_D — Mathlib

English

The liftKaehlerDifferential composed with D equals the identity map on the Kaehler setup.

Русский

Сложение liftKaehlerDifferential с D даёт тождественное отображение.

LaTeX

$$D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = LinearMap.id$$

Lean4

theorem liftKaehlerDifferential_D : (KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id :=
  Derivation.liftKaehlerDifferential_unique _ _ (KaehlerDifferential.D R S).liftKaehlerDifferential_comp

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