coeff_mapRange — Mathlib

English

Applying a range-map to a polynomial commutes with taking a coefficient: coeff m (mapRange g hg φ) = g (coeff m φ).

Русский

Применение отображения диапазона к многочлену и взятие коэффициента взаимно однозначны: coeff m (mapRange g hg φ) = g (coeff m φ).

LaTeX

$$$\forall g\ hg\ φ:\ \mathrm{coeff}\;m (\mathrm{mapRange}\ g\ hg\ φ) = g (\mathrm{coeff}\;m\ φ)$$$

Lean4

@[simp]
theorem coeff_mapRange (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) (m) :
    coeff m (mapRange g hg φ) = g (coeff m φ) := by simp [mapRange, coeff]

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