laurent_at_zero

Mathlib.FieldTheory.Laurent

URI: https://scilib.ai/kg/mathlib#RatFunc.laurent_at_zero

English

For all f in RatFunc R, laurent 0 f = f.

Русский

Для любого f ∈ RatFunc R верно laurent 0 f = f.

LaTeX

$$$\\mathrm{laurent}\\!\\_0 f = f.$$$

Lean4

@[simp]
theorem laurent_at_zero : laurent 0 f = f := by induction f using RatFunc.induction_on; simp

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

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

Разделы

Аффилиация

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