prod — Mathlib

English

The pointwise product of two TypeVecs: (α × α′) at index i is the pair (α i, α′ i), with recursive structure along the length.

Русский

Покомпонентно произведение двух TypeVec: на каждом индексе i получаем пару (α i, α′ i).

LaTeX

$$$$\\text{prod}: \\forall n,\\ TypeVec(n) \\to TypeVec(n) \\to TypeVec(n)\\,.$$

Lean4

/-- `prod α β` is the pointwise product of the components of `α` and `β` -/
def prod : ∀ {n}, TypeVec.{u} n → TypeVec.{u} n → TypeVec n
  | 0, _, _ => Fin2.elim0
  | n + 1, α, β => (@prod n (drop α) (drop β)) ::: (last α × last β)

Похожие утверждения