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)