map_toSubring — Mathlib

English

Mapping the toSubring polynomial back via the natural inclusion gives the original polynomial.

Русский

Отображение через встроенное включение обратно в исходное множество восстанавливает исходный полином.

LaTeX

$$$\\bigl(\\mathrm{toSubring}\\ p\\ hp\\bigr).\\mathrm{map}(\\mathrm{Subring.subtype}\\ T) = p$$$

Lean4

@[simp]
theorem map_toSubring : (p.toSubring T hp).map (Subring.subtype T) = p :=
  by
  ext n
  simp [coeff_map]

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