kerTotal_mkQ_single_smul — Mathlib

English

Scalar multiplication distributes through the differential kernel: (r × x)⟂ = r × x⟂.

Русский

Умножение на скаляр распределяется через ядро дифференциала: (r × x)⟂ = r × (x⟂).

LaTeX

$$$ (r \\cdot x)\\_\\mathcal{D} = r \\cdot x\\_\\mathcal{D} $$$

Lean4

theorem kerTotal_mkQ_single_smul (r : R) (x y) : (y𝖣r • x) = r • y𝖣x :=
  by
  letI : SMulZeroClass R S := inferInstance
  rw [Algebra.smul_def, KaehlerDifferential.kerTotal_mkQ_single_mul, KaehlerDifferential.kerTotal_mkQ_single_algebraMap,
    add_zero, ← LinearMap.map_smul_of_tower, Finsupp.smul_single, mul_comm, Algebra.smul_def]

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