distribMulAction' — Mathlib

English

Scalar multiplication distributes over addition: r • (x + y) = r • x + r • y.

Русский

Скалярное умножение распределяется по сложению: r • (x + y) = r • x + r • y.

LaTeX

$$$ r \cdot (x+y) = r \cdot x + r \cdot y $$$

Lean4

instance distribMulAction' : DistribMulAction R₁ (⨂[R] i, s i)
    where
  smul := (· • ·)
  smul_add _ _ _ := AddMonoidHom.map_add _ _ _
  mul_smul r r'
    x :=
    PiTensorProduct.induction_on' x (fun {r'' f} ↦ by simp [smul_tprodCoeff', smul_smul]) fun {x y} ihx ihy ↦ by
      simp_rw [PiTensorProduct.smul_add, ihx, ihy]
  one_smul
    x :=
    PiTensorProduct.induction_on' x (fun {r f} ↦ by rw [smul_tprodCoeff', one_smul]) fun {z y} ihz ihy ↦ by
      simp_rw [PiTensorProduct.smul_add, ihz, ihy]
  smul_zero _ := AddMonoidHom.map_zero _

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