General_Distributivity_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

abstract-algebradistributive-operationsgeneral-distributivity-theoremnamed-theoremsproofwikisummations

$\displaystyle \paren {\sum_{i \mathop = 1}^m a_i} * \paren {\sum_{j \mathop = 1}^n b_j} = \sum_{ {1 \mathop \le i \mathop \le m} \atop {1 \mathop \le j \mathop \le n} } \paren {a_i * b_j}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem General_Distributivity_Theorem {R : Type _} [CommRing R] (a b c d : R) : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by sorry

Source

https://proofwiki.org/wiki/General_Distributivity_Theorem

View graph