constantCoeff_rename — Mathlib

English

The constant term is preserved by renaming: constantCoeff (rename f φ) = constantCoeff φ.

Русский

Постоянная часть сохраняется при переименовании: constantCoeff (rename f φ) = constantCoeff φ.

LaTeX

$$$ constantCoeff (rename f \phi) = constantCoeff \phi $$$

Lean4

@[simp]
theorem constantCoeff_rename {τ : Type*} (f : σ → τ) (φ : MvPolynomial σ R) :
    constantCoeff (rename f φ) = constantCoeff φ :=
  by
  apply φ.induction_on
  · intro a
    simp only [constantCoeff_C, rename_C]
  · intro p q hp hq
    simp only [hp, hq, map_add]
  · intro p n hp
    simp only [hp, rename_X, constantCoeff_X, map_mul]

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