quotKerTotalEquiv_symm_comp_D — Mathlib

English

Equivalence of quotients and derivations under a symmetry of the quotient kernel: a lift equality holds with composition.

Русский

Эквивалентность квотирования и производных с учётом симметрии ядра, выполняется равенство композиции с подстановкой.

LaTeX

$$$(\\mathrm{quotKerTotalEquiv}(R,S))^{-1}.toLinearMap \\circ \\mathrm{compDer} \\big( \\mathrm{D}(R,S) \\big) = \\mathrm{derivationQuotKerTotal}(R,S)$$$

Lean4

theorem quotKerTotalEquiv_symm_comp_D :
    (KaehlerDifferential.quotKerTotalEquiv R S).symm.toLinearMap.compDer (KaehlerDifferential.D R S) =
      KaehlerDifferential.derivationQuotKerTotal R S :=
  by convert (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential_comp

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