taylorEquiv — Mathlib

English

Taylor shift at r defines an algebra isomorphism of the polynomial ring: taylorEquiv r: R[X] ≃ₐ[R] R[X].

Русский

Сдвиг ряда Тейлора по r определяет алгебраическое изоморфизм кольца полиномов: taylorEquiv r : R[X] ≃ₐ[R] R[X].

LaTeX

$$$$ \\mathrm{taylorEquiv}(r) : R[X] \\cong_{R} R[X] \\text{ is an algebra automorphism with inverse } \\mathrm{taylorEquiv}(-r). $$$$

Lean4

/-- `Polynomial.taylor` as an `AlgEquiv` for commutative rings. -/
noncomputable def taylorEquiv (r : R) : R[X] ≃ₐ[R] R[X]
    where
  invFun := taylorAlgHom (-r)
  left_inv P := by simp [taylor, comp_assoc]
  right_inv P := by simp [taylor, comp_assoc]
  __ := taylorAlgHom r

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