natDegree_pos_iff_degree_pos

Mathlib.Algebra.Polynomial.Degree.Definitions

URI: https://scilib.ai/kg/mathlib#Polynomial.natDegree_pos_iff_degree_pos

English

0 < natDegree p ↔ 0 < degree p.

Русский

0 < natDegree p эквивалентно 0 < degree p.

LaTeX

$$0 < natDegree(p) ↔ 0 < degree(p)$$

Lean4

theorem natDegree_pos_iff_degree_pos : 0 < natDegree p ↔ 0 < degree p :=
  lt_iff_lt_of_le_iff_le natDegree_le_iff_degree_le

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

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

Разделы

Аффилиация

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