map_taylorEquiv_degreeLT — Mathlib

English

The map taylorEquiv sends the degreeLT subspace to itself: map (taylorEquiv r) (degreeLT R n) = degreeLT R n.

Русский

Отображение taylorEquiv отправляет подпространство degreeLT в себя: map (taylorEquiv r) (degreeLT R n) = degreeLT R n.

LaTeX

$$$\\text{map }(\\text{taylorEquiv } r) (\\text{degreeLT } R n) = \\text{degreeLT } R n.$$$

Lean4

theorem map_taylorEquiv_degreeLT : (R[X]_n).map (taylorEquiv r) = R[X]_n := by
  nth_rw 1 [← comap_taylorEquiv_degreeLT (r := r), Submodule.map_comap_eq_of_surjective (taylorEquiv r).surjective]

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