add_tprodCoeff — Mathlib

English

For a fixed index i, adding updates at i to two elements m1 and m2 is the same as updating i with the sum m1+m2 in tprodCoeff.

Русский

Для фиксированного индекса i сложение обновлений в i двух элементов m1 и m2 эквивалентно обновлению i на сумму m1+m2 в tprodCoeff.

LaTeX

$$$tprodCoeff(R,z,update f i m_1) + tprodCoeff(R,z,update f i m_2) = tprodCoeff(R,z,update f i (m_1+m_2))$$$

Lean4

theorem add_tprodCoeff [DecidableEq ι] (z : R) (f : Π i, s i) (i : ι) (m₁ m₂ : s i) :
    tprodCoeff R z (update f i m₁) + tprodCoeff R z (update f i m₂) = tprodCoeff R z (update f i (m₁ + m₂)) :=
  Quotient.sound' <| AddConGen.Rel.of _ _ (Eqv.of_add _ z f i m₁ m₂)

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