ofVector — Mathlib

English

There is a quotient map from List.Vector α n to Sym α n, sending a vector to the corresponding symmetric power element.

Русский

Существует факторное отображение от List.Vector α n к Sym α n, отправляющее вектор в соответствующий элемент симметрической мощности.

LaTeX

$$$ \mathrm{ofVector}: \mathrm{List.Vector}(\alpha,n) \to \mathrm{Sym}(\alpha,n) $$$

Lean4

/-- This is the quotient map that takes a list of n elements as an n-tuple and produces an nth
symmetric power.
-/
def ofVector : List.Vector α n → Sym α n := fun x => ⟨↑x.val, (Multiset.coe_card _).trans x.2⟩

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