instDistrib — Mathlib

English

Product of two distributive types is distributive.

Русский

Произведение двух дистрибутивных типов является дистрибутивным.

LaTeX

$$$\text{Distrib}(R \times S)$$$

Lean4

/-- Product of two distributive types is distributive. -/
instance instDistrib [Distrib R] [Distrib S] : Distrib (R × S)
    where
  left_distrib _ _ _ := by ext <;> exact left_distrib ..
  right_distrib _ _ _ := by ext <;> exact right_distrib ..

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