ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4041 on D1239: Standard N-operation
Commutativity of finite basic real summation for two sums