kerTotal_mkQ_single_add — Mathlib

English

For elements x,y,z in the ambient algebra, a certain kernel-related construction is additive in its second component: (z ⟂ x) + y = (z ⟂ x) + z ⟂ y.

Русский

Для элементов x,y,z в алгебре существует свойство, что выражение, связанное с ядерной операцией, распределено по сумме во втором аргументе: (z ⟂ x) + y = (z ⟂ x) + z ⟂ y.

LaTeX

$$$(z\\triangleright x) + y = (z\\triangleright x) + z\\triangleright y$$$

Lean4

theorem kerTotal_mkQ_single_add (x y z) : (z𝖣x + y) = (z𝖣x) + z𝖣y :=
  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_add, ← smul_sub]
  exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inl <| ⟨⟨_, _⟩, rfl⟩))

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