num_zero

Mathlib.FieldTheory.RatFunc.Basic

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

English

The numerator of the zero rational function is zero.

Русский

Числитель нулевой рациональной функции равен нулю.

LaTeX

$$$\operatorname{num}(0) = 0$$$

Lean4

@[simp]
theorem num_zero : num (0 : RatFunc K) = 0 := by convert num_div' (0 : K[X]) one_ne_zero <;> simp

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

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

Разделы

Аффилиация

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