English
If z, f, i, r are as in the theorem, then tprodCoeff with update at i by r•f_i equals the tensor product with scalar r acting on z.
Русский
Если z, f, i, r как в теореме, тогда tprodCoeff с обновлением i на r•f_i равен тензорному произведению с действием скаляра r на z.
LaTeX
$$tprodCoeff(R,z,update f i (r•f i)) = tprodCoeff(R, r•z, f)$$
Lean4
theorem smul_tprodCoeff [DecidableEq ι] (z : R) (f : Π i, s i) (i : ι) (r : R₁) [SMul R₁ R] [IsScalarTower R₁ R R]
[SMul R₁ (s i)] [IsScalarTower R₁ R (s i)] : tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • z) f :=
by
have h₁ : r • z = r • (1 : R) * z := by rw [smul_mul_assoc, one_mul]
have h₂ : r • f i = (r • (1 : R)) • f i := (smul_one_smul _ _ _).symm
rw [h₁, h₂]
exact smul_tprodCoeff_aux z f i _
