comap_taylorEquiv_degreeLT — Mathlib

English

The comap of the taylorEquiv with degreeLT equals degreeLT: comap(taylorEquiv r)(degreeLT R n) = degreeLT R n.

Русский

Комаппинг taylorEquiv с degreeLT равен degreeLT: comap(taylorEquiv r)(degreeLT R n) = degreeLT R n.

LaTeX

$$$(\\text{Submodule}.comap (\\text{Polynomial.taylorEquiv } r) (\\text{Polynomial.degreeLT } R n)) = (\\text{Polynomial.degreeLT } R n).$$$

Lean4

theorem comap_taylorEquiv_degreeLT : (R[X]_n).comap (taylorEquiv r) = R[X]_n := by ext; simp [taylorEquiv]

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