English
Abbreviation: given a linearly ordered index set I and a function v: I → M, for any n and any Finset s ⊆ I with card s = n, ιMulti_family(n) v s equals the exterior product of v(i) over i in s, arranged according to the order of s.
Русский
Сокращение: задано линейно упорядоченное множество индексов I и функция v: I → M; для любого n и конечного подмножества s ⊆ I мощности n элементы ιMulti_family(n) v s равны внешнему произведению элементов v(i) по i из s в порядке s.
LaTeX
$$$ \\iotaMulti\\_family(R)(n)(v)(s) = \\iotaMulti(R,n)\\big(i \\mapsto v(\\mathrm{orderIsoOfFin} _ s.prop(i))\\big). $$$
Lean4
/-- Given a linearly ordered family `v` of vectors of `M` and a natural number `n`, produce the
family of `n`fold exterior products of elements of `v`, seen as members of the exterior algebra. -/
abbrev ιMulti_family (n : ℕ) {I : Type*} [LinearOrder I] (v : I → M) (s : { s : Finset I // Finset.card s = n }) :
ExteriorAlgebra R M :=
ιMulti R n fun i => v (Finset.orderIsoOfFin _ s.prop i)
