English
Renaming commutes with expansion: applying a rename before or after expansion yields the same polynomial.
Русский
Переименование и расширение коммутируют: применение переименования до/после расширения даёт одинаковый полином.
LaTeX
$$$$ \operatorname{rename}(f)(\operatorname{expand}(p)(\phi)) = \operatorname{expand}(p)(\operatorname{rename}(f)(\phi)). $$$$
Lean4
@[simp]
theorem rename_expand (f : σ → τ) (p : ℕ) (φ : MvPolynomial σ R) : rename f (expand p φ) = expand p (rename f φ) := by
simp [expand, bind₁_rename, rename_bind₁, Function.comp_def]