map_restriction — Mathlib

English

If you take a polynomial p and restrict its coefficients to a subring, then map the restricted polynomial back to the original ring, you recover p.

Русский

Если ограничить коэффициенты полинома p до подкольца, а затем вернуть его в исходное кольцо через отображение, то получается p.

LaTeX

$$$\\mathrm{map}(\\mathrm{algebraMap}\\,\\_\\,)(\\mathrm{restriction}(p)) = p$$$

Lean4

@[simp]
theorem map_restriction {R : Type u} [CommRing R] (p : R[X]) : p.restriction.map (algebraMap _ _) = p :=
  ext fun n => by rw [coeff_map, Algebra.algebraMap_ofSubring_apply, coeff_restriction]

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