sound — Mathlib

English

Let a,b be length-n vectors over α. If a.val is permutation-equivalent to b.val, then they determine the same element in the nth symmetric power: ↑a = ↑b in Sym α n.

Русский

Пусть a,b — векторы длины n над α. Если a.val эквивалентен b.val по перестановкам, то их образы в n-й симметрической степени совпадают: ↑a = ↑b.

LaTeX

$$$ a.\text{val} \sim b.\text{val} \Rightarrow \uparrow a = \uparrow b. $$$

Lean4

theorem sound {a b : List.Vector α n} (h : a.val ~ b.val) : (↑a : Sym α n) = ↑b :=
  Subtype.ext <| Quotient.sound h

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