English
If n = m (via h), then Sym α n is canonically equivalent to Sym α m by keeping the multiset and adjusting the length proof using h.
Русский
Если n = m через некоторое равенство h, то Sym α n естественным образом эквивалентно Sym α m, сохраняя множественный набор и корректируя доказательство длины через h.
LaTeX
$$$\\mathrm{Sym.cast}~h : \\mathrm{Sym} \\;\\alpha\\; n \\simeq \\mathrm{Sym} \\;\\alpha\\; m$, где $\\mathrm{toFun}(s) = \\langle s.1, s.2 \\rangle$ с заменой доказательства длины на $s.2 \\circ h$; обращение аналогично с $h^{-1}$.$$
Lean4
/-- Change the length of a `Sym` using an equality.
The simp-normal form is for the `cast` to be pushed outward. -/
protected def cast {n m : ℕ} (h : n = m) : Sym α n ≃ Sym α m
where
toFun s := ⟨s.val, s.2.trans h⟩
invFun s := ⟨s.val, s.2.trans h.symm⟩
