How to introduce a list of numbers or a list of functions?

Stream: new members

[Yagub Aliyev]

What is the best way to introduce a list (or a finite sequence) of rationals a[i] b[i]: ℚ and functions f[i](x) =a[i]*x+b[i] from ℚ to ℚ?

[Eric Wieser]

a b : Fin n -> ℚ might be a good choice for the sequence

[Yagub Aliyev]

Should n be introduced before? What about functions?

import Mathlib
lemma formula1 (n : ℕ) (x : ℚ) (a b : Fin n -> ℚ)

[Eric Wieser]

Do you want to "introduce" a function, or "define" a function?

[Eric Wieser]

Your = suggests the latter

[Yagub Aliyev]

Sorry, I am still learning the terminology. Yes, define. I have a formula for it f[i](x) =a[i]*x+b[i].

[Eric Wieser]

def f {n : ℕ} (a b : Fin n -> ℚ) (i : Fin n) (x : ℚ) : ℚ := a i * x + b i

should work

[Eric Wieser]

Here, your $f[i](x)$ is f a b i x

[Yagub Aliyev]

Thank you! I have plans to work with indices modulo n so I want them be between 0 and n-1. Is there a way to make Lean to start i from 0?

[Eric Wieser]

It already does :)

[Eric Wieser]

docs#Fin

[Yagub Aliyev]

Oh! I am so lucky! :-)