smul_tprodCoeff_aux — Mathlib

English

Introduce a scalar action of R1 on the tensor product ⨂_R s_i, compatible with the tower of algebras.

Русский

Введено действие скаляра R1 на тензорное произведение ⨂_R s_i, совместимое с башней алгебр.

LaTeX

$$$\exists (r:\, R_1), \; r \cdot (x) = \text{something compatible}$$$

Lean4

theorem smul_tprodCoeff_aux [DecidableEq ι] (z : R) (f : Π i, s i) (i : ι) (r : R) :
    tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r * z) f :=
  Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _ _ _

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