intDegree_zero

Mathlib.FieldTheory.RatFunc.Degree

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

English

The degree of the zero rational function is zero.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem intDegree_zero : intDegree (0 : RatFunc K) = 0 := by
  rw [intDegree, num_zero, natDegree_zero, denom_zero, natDegree_one, sub_self]

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

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

Разделы

Аффилиация

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