coe_taylorAlgHom — Mathlib

English

The equality taylorAlgHom r = taylor r holds, i.e., the Taylor shift viewed as an algebra hom equals the underlying Taylor operator.

Русский

Ряд Тейлора, рассмотренный как алгебраический гомоморфизм, равен линейному оператору Taylor: taylorAlgHom r = taylor r.

LaTeX

$$$$ \\operatorname{taylorAlgHom}(r) = \\operatorname{taylor}(r). $$$$

Lean4

@[simp, norm_cast]
theorem coe_taylorAlgHom : taylorAlgHom r = taylor r :=
  rfl

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