natDegree_le_iff_degree_le — Mathlib

English

Let p be a polynomial over a semiring R. Then natDegree p ≤ n if and only if degree p ≤ n.

Русский

Пусть p — полином над полукольцом R. Тогда natDegree p ≤ n эквивалентно degree p ≤ n.

LaTeX

$$$\\operatorname{natDegree}(p) \\le n \\;\\Longleftrightarrow\\; \\operatorname{degree}(p) \\le n$$$

Lean4

theorem natDegree_le_iff_degree_le {n : ℕ} : natDegree p ≤ n ↔ degree p ≤ n :=
  WithBot.unbotD_le_iff (fun _ ↦ bot_le)

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