instCoeVector — Mathlib

English

There is a canonical coercion from List.Vector α n to Sym α n.

Русский

Существует каноническое вложение List.Vector α n в Sym α n.

LaTeX

$$$ \text{there is a canonical } \mathrm{Coe}: \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.
-/
instance : Coe (List.Vector α n) (Sym α n) where coe x := ofVector x

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