To List or not to List?

Stream: Is there code for X?

[J. J. Issai (project started by GRP)]

I am working on some definitions in number theory (so all variables are based on Nat) and I would like to know what idiom to use.
First up is defining a certain kind of arithmetic progression. This beast has $k$ terms of the form $n+id$ for $1\le i \le k$ and with $\gcd(n,d)=1$. For now and for this thread I am willing to work with $n>0$ (later I would like to have $n > -d$). For reasons of exposition, I would like the index to range from 1 to k. Here is a suggestion from Harmonic's Aristotle:

def isIrreducibleBigAP (n d k : ℕ) (s : List ℕ) : Prop :=
  s = (List.range k).map (fun i => n + (i + 1) * d) ∧ n.gcd d = 1

At the moment, I have two use cases for this: taking the product $\prod_{1\le i \le k} (n+id)$, and generating another sequence I want to analyze (In leanspeak, something like (List.range k).map (fun i +> g ( n + (i+1)*d ) ) ) . I would prefer not to have the definition shift the internal indexing to (0..k-1) from (1..k). Can I use something based on Icc 1 k, or some other idiom I need to learn? Also what are the downsides of the List idiom or another idiom in terms of dealing with making a Lean proof?

[Yury G. Kudryashov]

While you can use \prod j \in Finset.Icc 1 k, f j, the API works much better if you start indexes with 0.

[Yury G. Kudryashov]

I would reconsider reindexing from 0.

[Yury G. Kudryashov]

Also, do you want a predicate or a definition? What kind of statements do you want to formulate? Are you going to submit it to Mathlib? Some other repo? An AI company? Something else?

[Yury G. Kudryashov]

The last question affects coding style decisions a lot.

[J. J. Issai (project started by GRP)]

Right now the answer is "something else". If the results are useful for Mathlib or some other organization, then I am likely to turn the results over for refactoring by someone else. However, I want to use this as an example to teach others, and so I want to follow the notation from the literature. Also, some results don't hold if I use n+id for 0<=i<k . So I am at present attached to the literature indexing (which has n+d, n+2d, ..., n+kd) and am hoping for a different idiom.

One statement I am working towards has the shape: if <n+id> is an irreducible arithmetic progression and (some other property), then <g(n+id)> (g mapping on <n+id>) is a sequence with duplicate entries. (I am omitting the indexing right now for brevity.)