taylor_zero'

Mathlib.Algebra.Polynomial.Taylor

URI: https://scilib.ai/kg/mathlib#Polynomial.taylor_zero'

English

Taylor at 0 is the identity map, i.e., taylor 0 = id.

Русский

Тейлор в нуле есть тождественное отображение, то есть taylor 0 = id.

LaTeX

$$$$ \operatorname{taylor}(0) = \operatorname{id} $$$$

Lean4

@[simp]
theorem taylor_zero' : taylor (0 : R) = LinearMap.id :=
  LinearMap.ext taylor_zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru