map_mapRange_eq_iff — Mathlib

English

Characterizes when map f on Finsupp.mapRange g maps back to φ; precisely, map f (Finsupp.mapRange g hg φ) = φ iff ∀ d, f(g(coeff d φ)) = coeff d φ.

Русский

Характеризуется, когда отображение map f на Finsupp.mapRange g hg φ возвращает φ; эквивалентно: ∀ d, f(g(coeff d φ)) = coeff d φ.

LaTeX

$$$ map f (Finsupp.mapRange g hg \\phi) = \\phi \\\\Longleftrightarrow \\forall d, f(g(\\\\mathrm{coeff} \\\\ d \\\\phi)) = \\\\mathrm{coeff} \\\\ d \\\\phi $$$

Lean4

theorem map_mapRange_eq_iff (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
    map f (Finsupp.mapRange g hg φ) = φ ↔ ∀ d, f (g (coeff d φ)) = coeff d φ := by
  simp_rw [MvPolynomial.ext_iff, coeff_map, coeff_mapRange]

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