rename_expand — Mathlib

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]

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