taylorLinearEquiv — Mathlib

English

The map taylor r induces an automorphism of the submodule R[X]_n, i.e., an R-linear isomorphism R[X]_n ≃ R[X]_n.

Русский

Отображение Taylor r порождает автоморфизм подмодуля R[X]_n, т.е. линейное изоморфизм R[X]_n ≃ R[X]_n.

LaTeX

$$$\\text{taylorLinearEquiv } (r) : R[X]_n \\simeq_R R[X]_n$.$$

Lean4

/-- The map `taylor r` induces an automorphism of the module `R[X]_n` of polynomials of
degree `< n`. -/
@[simps! apply_coe]
noncomputable def taylorLinearEquiv (r : R) (n : ℕ) : R[X]_n ≃ₗ[R] R[X]_n :=
  (taylorEquiv r : R[X] ≃ₗ[R] R[X]).ofSubmodules _ _ map_taylorEquiv_degreeLT

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