How to Formalize Sequence?

Stream: new members

[mathnoter]

I am trying to formalize a sequence problem in Lean 4. For example, given that \( a_n = 2n + 1 \), I want to find the sum \( a_1 + \ldots + a_n \). Is the best approach to represent this sequence using (a : Fin n → ℝ)? How should I go about formalizing this type of problem?

Additionally, where can I find examples of proofs related to sequences to help with my learning?

Thank you!

[Johan Commelin]

Your sequence would be

def a (n : Nat) : ℝ := 2 * n + 1

and you can take the sum with

variable (n : Nat)
#check ∑ i in Finset.range n, a i