English
The product of a indexed sum (Sigma-type) by a fixed type γ is equivalent to the Sigma-type of indexed products: (Σ i, α i) × γ ≃ Σ i, α i × γ.
Русский
Произведение индексированной суммы (типы Σ i, α i) на фиксированную γ эквивалентно сумме произведений: (Σ i, α i) × γ ≃ Σ i, α i × γ.
LaTeX
$$$\big(\sum_{i} \alpha(i)\big) \times \gamma \cong \sum_{i} (\alpha(i) \times \gamma).$$$
Lean4
/-- The product of an indexed sum of types (formally, a `Sigma`-type `Σ i, α i`) by a type `β` is
equivalent to the sum of products `Σ i, (α i × β)`. -/
@[simps apply symm_apply]
def sigmaProdDistrib {ι : Type*} (α : ι → Type*) (β : Type*) : (Σ i, α i) × β ≃ Σ i, α i × β :=
⟨fun p => ⟨p.1.1, (p.1.2, p.2)⟩, fun p => (⟨p.1, p.2.1⟩, p.2.2), by grind, by grind⟩
