trunc_zero'

Mathlib.RingTheory.PowerSeries.Trunc

URI: https://scilib.ai/kg/mathlib#PowerSeries.trunc_zero'

English

The zero polynomial is the truncation at 0 for any f.

Русский

Нулевой полином равен усечению нуля для любого f.

LaTeX

$$$\\operatorname{trunc}_0 f = 0$$$

Lean4

@[simp]
theorem trunc_zero' {f : R⟦X⟧} : trunc 0 f = 0 :=
  rfl

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

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

Разделы

Аффилиация

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