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₂)