ext — Mathlib

English

Let s1 and s2 be elements of the nth symmetric power Sym α n. If their underlying multisets are equal, then s1 = s2.

Русский

Пусть s1 и s2 являются элементами n-й симметрической мощности Sym α n. Если их соответствующие мультисеты совпадают, то s1 = s2.

LaTeX

$$$ (s_1 : \mathrm{Multiset}(\alpha)) = (s_2 : \mathrm{Multiset}(\alpha)) \Rightarrow s_1 = s_2 $$$

Lean4

@[ext]
theorem ext {s₁ s₂ : Sym α n} (h : (s₁ : Multiset α) = ↑s₂) : s₁ = s₂ :=
  coe_injective h

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