prodSumDistrib — Mathlib

English

Type product is left distributive with respect to type sum up to an equivalence: α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ).

Русский

Дистрибутивность произведения слева над суммой: α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ).

LaTeX

$$$$\alpha \times (\beta \oplus \gamma) \simeq (\alpha \times \beta) \oplus (\alpha \times \gamma).$$$$

Lean4

/-- Type product is left distributive with respect to type sum up to an equivalence. -/
def prodSumDistrib (α β γ) : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ) :=
  calc
    α × (β ⊕ γ) ≃ (β ⊕ γ) × α := prodComm _ _
    _ ≃ (β × α) ⊕ (γ × α) := (sumProdDistrib _ _ _)
    _ ≃ (α × β) ⊕ (α × γ) := sumCongr (prodComm _ _) (prodComm _ _)

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