Sums of finite sequences of real numbers

Content created by Louis Wasserman.

Created on 2025-12-25.
Last modified on 2025-12-25.

module real-numbers.sums-of-finite-sequences-of-real-numbers where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups

open import lists.finite-sequences

open import real-numbers.dedekind-real-numbers
open import real-numbers.large-additive-group-of-real-numbers

Idea

The sum operation extends the operation of addition on the real numbers to any finite sequence of real numbers.

Definition

sum-fin-sequence-ℝ : {l : Level} (n : ℕ) → fin-sequence (ℝ l) n → ℝ l
sum-fin-sequence-ℝ {l} = sum-fin-sequence-type-Ab (ab-add-ℝ l)
  • Sum at Wikidata

Recent changes