leftDistribClass — Mathlib

English

In a structure with Mul and Add that satisfies a LeftDistribClass, left distributivity holds: a*(b+c) = a*b + a*c for all a,b,c.

Русский

В структуре с умножением и сложением, удовлетворяющей LeftDistribClass, выполняется левое распределение: a*(b+c) = a*b + a*c для всех a,b,c.

LaTeX

$$$a \cdot (b + c) = a \cdot b + a \cdot c$$$

Lean4

instance (priority := 100) leftDistribClass (R : Type*) [Distrib R] : LeftDistribClass R :=
  ⟨Distrib.left_distrib⟩
    -- see Note [lower instance priority]

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