English
The sym2 of a singleton equals the singleton of the replicated element.
Русский
Sym2 от единичного множества равен единичному набору повторённого элемента.
LaTeX
$$({a} : Finset α).sym n = {Sym.replicate n a}$$
Lean4
@[simp]
theorem sym_singleton (a : α) (n : ℕ) : ({ a } : Finset α).sym n = {Sym.replicate n a} :=
eq_singleton_iff_unique_mem.2
⟨replicate_mem_sym (mem_singleton.2 rfl) _, fun _s hs ↦
Sym.eq_replicate_iff.2 fun _b hb ↦ eq_of_mem_singleton <| mem_sym_iff.1 hs _ hb⟩