English
For fixed degree n, the image of ExteriorAlgebra.ιMulti R n spans the nth exterior power ∧^n_R M; equivalently, the submodule generated by the images of ExteriorAlgebra.ιMulti R n is all of ∧^n_R M.
Русский
Для фиксированной степени n образ ExteriorAlgebra.ιMulti R n порождает ∧^n_R M; другими словами, порождаемая образами ιMulti R n подмодуль равен всём ∧^n_R M.
LaTeX
$$$\operatorname{span}_R(\operatorname{range}(ExteriorAlgebra.ιMulti R n)) = \bigwedge^n_R M$$$
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
`n`th exterior power. -/
noncomputable def ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (s : { s : Finset I // Finset.card s = n }) :
⋀[R]^n M :=
ιMulti R n fun i ↦ v <| Finset.orderIsoOfFin s.val s.property i
