kerTotal_mkQ_single_mul — Mathlib

English

The kernel total map applied to a single product distributes as a sum of two terms with the product in the second slot.

Русский

Ядро полной карты применённой к одиночному произведению дистрибуирует как сумма двух членa, где произведение находится во втором слоте.

LaTeX

$$$\\text{kerTotal}_R^S(xy) = (y)\\_R^S(x) + (x)\\_R^S(y)$$$

Lean4

theorem kerTotal_mkQ_single_mul (x y z) : (z𝖣x * y) = ((z * x)𝖣y) + (z * y)𝖣x :=
  by
  rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)), Submodule.mkQ_apply,
    Submodule.Quotient.mk_eq_zero]
  simp_rw [← Finsupp.smul_single_one _ z, ← @smul_eq_mul _ _ z, ← Finsupp.smul_single, ← smul_add, ← smul_sub]
  exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inr <| ⟨⟨_, _⟩, rfl⟩))

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