hasSMul' — Mathlib

English

A scalar action of R on the tensor product ⨂_R s_i is defined compatibly with the tower, enabling module structure.

Русский

Определено действие скаляра R на тензорное произведение ⨂_R s_i, совместимое с башней алгебр, образующее модульную структуру.

LaTeX

$$$\text{SMul} \; R_1 (\otimes_R s_i)$ exists and is compatible$$

Lean4

instance hasSMul' : SMul R₁ (⨂[R] i, s i) :=
  ⟨fun r ↦
    liftAddHom (fun f : R × Π i, s i ↦ tprodCoeff R (r • f.1) f.2)
      (fun r' f i hf ↦ by simp_rw [zero_tprodCoeff' _ f i hf]) (fun f ↦ by simp [zero_tprodCoeff])
      (fun r' f i m₁ m₂ ↦ by simp [add_tprodCoeff]) (fun r' r'' f ↦ by simp [add_tprodCoeff']) fun z f i r' ↦ by
      simp [smul_tprodCoeff, mul_smul_comm]⟩

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