deg_pos

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRootMonic.deg_pos

English

If S is nontrivial and h is IsAdjoinRootMonic S f, then the degree of f is positive: natDegree f > 0.

Русский

Если S ненулево и h является IsAdjoinRootMonic S f, то порядок f положителен: natDegree f > 0.

LaTeX

$$$0 < \\operatorname{natDegree} f$$$

Lean4

theorem deg_pos [Nontrivial S] : 0 < natDegree f :=
  by
  rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩
  exact Nat.zero_lt_of_lt hi

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

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

Разделы

Аффилиация

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