English
For any f, p, the renamed polynomial equals applying double mapDomain: rename_f p = Finsupp.mapDomain (Finsupp.mapDomain f) p.
Русский
Для любого f и p переименование полиномa эквивалентно двойному применению mapDomain: rename_f p = Finsupp.mapDomain (Finsupp.mapDomain f) p.
LaTeX
$$$\\text{rename } f\, p = \\mathrm{Finsupp.mapDomain}(\\mathrm{Finsupp.mapDomain} f)\\, p.$$$
Lean4
/-- `MvPolynomial.rename e` is an equivalence when `e` is. -/
@[simps apply]
def renameEquiv (f : σ ≃ τ) : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R :=
{ rename f with
toFun := rename f
invFun := rename f.symm
left_inv := fun p => by rw [rename_rename, f.symm_comp_self, rename_id_apply]
right_inv := fun p => by rw [rename_rename, f.self_comp_symm, rename_id_apply] }
