finsuppLeft_smul' — Mathlib

English

The left-side isomorphism is linear with respect to the scalar S in an IsScalarTower setup: finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t.

Русский

Левый изоморфизм линейный по скалярному действию в S в конфигурации IsScalarTower: finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t.

LaTeX

$$$ finsuppLeft R M N ι (s \\cdot t) = s \\cdot finsuppLeft R M N ι t $$$

Lean4

theorem finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) : finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t := by
  induction t with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | tmul p n => ext; simp [smul_tmul', finsuppLeft_apply_tmul_apply]

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