zero_tprodCoeff — Mathlib

English

PiTensorProduct carries an AddCommMonoid structure componentwise, i.e., the sum in the PiTensorProduct corresponds to pointwise addition in the factors.

Русский

PiTensorProduct обладает структурой AddCommMonoid поэлементно: сумма в PiTensorProduct соответствует поэлементному сложению компонентов.

LaTeX

$$$\text{AddCommMonoid}(\bigoplus_{i} s_i) \cong \bigoplus_{i} (\text{AddCommMonoid}(s_i))$$$

Lean4

theorem zero_tprodCoeff (f : Π i, s i) : tprodCoeff R 0 f = 0 :=
  Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_scalar _

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