Prove2Me

lean_workbook_plus_75901

Proved

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

Does ∑j=1n∑i=1maij=∑i=1m∑j=1naij \displaystyle\sum_{j = 1}^n \displaystyle\sum_{i = 1}^m a_{ij}=\displaystyle\sum_{i = 1}^m \displaystyle\sum_{j = 1}^n a_{ij} hold for all n,m when aij≥0 ∀i,j a_{ij}\geq0 \ \forall i,j?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75901 (m n : ℕ) (a : Fin m → Fin n → NNReal) : ∑ j : Fin n, ∑ i : Fin m, a i j = ∑ i : Fin m, ∑ j : Fin n, a i j   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph