mul_right_distrib — Mathlib

English

Right distributivity of Holor multiplication over addition: (x + y) ⊗ z = x ⊗ z + y ⊗ z.

Русский

Правое распределение умножения Holor над сложением: (x + y) ⊗ z = x ⊗ z + y ⊗ z.

LaTeX

$$$ (x + y) \otimes z = x \otimes z + y \otimes z $$$

Lean4

theorem mul_right_distrib [Distrib α] (x : Holor α ds₁) (y : Holor α ds₁) (z : Holor α ds₂) :
    (x + y) ⊗ z = x ⊗ z + y ⊗ z :=
  funext fun t => add_mul (x t.take) (y t.take) (z t.drop)

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