rightDistribClass — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) rightDistribClass (R : Type*) [Distrib R] : RightDistribClass R :=
  ⟨Distrib.right_distrib⟩

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