mapRange_eq_map — Mathlib

English

For a polynomial p and a ring hom f, applying mapRange to the coefficients equals mapping the polynomial via f: Finsupp.mapRange f f.map_zero p = map f p.

Русский

При применении отображения коэффициентов к полиному через f получаем то же, что и полином, полученный через map f.

LaTeX

$$$Finsupp.mapRange\\ f\\ f.map_zero\\ p = map\\ f\\ p$$$

Lean4

theorem mapRange_eq_map {R S : Type*} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) :
    Finsupp.mapRange f f.map_zero p = map f p :=
  by
  rw [p.as_sum, Finsupp.mapRange_finset_sum, map_sum (map f)]
  refine Finset.sum_congr rfl fun n _ => ?_
  rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]

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