expand_monomial — Mathlib

English

Renaming variables commutes with expansion: renaming after expansion equals expanding after renaming.

Русский

Переименование переменных коммутирует с расширением: переименование после расширения равно расширению после переименования.

LaTeX

$$$$ \operatorname{rename}(f)(\operatorname{expand}(p)(\phi)) = \operatorname{expand}(p)(\operatorname{rename}(f)(\phi)). $$$$

Lean4

@[simp]
theorem expand_monomial (p : ℕ) (d : σ →₀ ℕ) (r : R) :
    expand p (monomial d r) = C r * ∏ i ∈ d.support, (X i ^ p) ^ d i :=
  bind₁_monomial _ _ _

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