derivationQuotKerTotal_lift_comp_linearCombination

English

Unit element maps to zero under kerTotal mkQ single amount: 1 ⟂ x = 0.

Русский

Единственный элемент отображается в нуль при kerTotal mkQ: 1 ⟂ x = 0.

LaTeX

$$$ (1)\\_\\mathcal{D}(x) = 0 $$$

Lean4

theorem derivationQuotKerTotal_lift_comp_linearCombination :
    (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential.comp
        (Finsupp.linearCombination S (KaehlerDifferential.D R S)) =
      Submodule.mkQ _ :=
  by
  apply Finsupp.lhom_ext
  intro a b
  conv_rhs => rw [← Finsupp.smul_single_one a b, LinearMap.map_smul]
  simp [KaehlerDifferential.derivationQuotKerTotal_apply]

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