taylorAlgHom — Mathlib

English

Taylor shift at r yields an algebra homomorphism from R[X] to R[X], i.e., a structure-preserving map.

Русский

Сдвиг Тейлора по r задаёт алгебраический гомоморфизм из R[X] в R[X].

LaTeX

$$$$ \\exists \\phi: R[X] \\to_{R} R[X],\\ \\phi \\text{ is an algebra hom and } \\phi(f) = \\operatorname{taylor}(r,f). $$$$

Lean4

/-- `Polynomial.taylor` as an `AlgHom` for commutative semirings -/
@[simps!]
def taylorAlgHom (r : R) : R[X] →ₐ[R] R[X] :=
  AlgHom.ofLinearMap (taylor r) (taylor_one r) (taylor_mul r)

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