mul_left_distrib — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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