theorem Fin.prod_add_eq_sum_prod_choice (d : ℕ) (a b : Fin d → ℝ) : ∏ i : Fin d, (a i + b i) = ∑ c : Fin d → Bool, ∏ i : Fin d, if c i = true then b i else a i

Distributive law: product of sums over Fin d equals sum over boolean choices of products. This is the key identity: ∏ᵢ (aᵢ + bᵢ) = ∑_{c : Fin d → Bool} ∏ᵢ (if cᵢ then bᵢ else aᵢ)