Name for iterated product

Stream: Is there code for X?

[Thomas Browning]

Does mathlib have a definition of the form

def iteratedProduct (α : Type u) : (n : ℕ) → Type u
  | 0 => PUnit
  | n + 1 => iteratedProduct α n × α

or is there nothing closer than Fin n → α?

[Aaron Liu]

I suppose Nat.below is something similar, but that's more of an implementation detail for structural recursion, not like an actual definition

[Sébastien Gouëzel]

docs#List.TProd (but normallywe try to avoid it unless there's a compelling reason)