instWellFoundedRelation

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

There is a canonical well-founded relation on polynomials given by degree.

Русский

Существует каноническое хорошо упорядоченное отношение на многочленах, задаваемое по степени.

LaTeX

$$$\\text{On } R[X], \\; p \\prec q \\iff \\operatorname{degree}(p) < \\operatorname{degree}(q).$$$

Lean4

instance : WellFoundedRelation R[X] :=
  ⟨_, degree_lt_wf⟩

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

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

Разделы

Аффилиация

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