two_le_natDegree_iff — Mathlib

English

Let S be a subalgebra of B and x be integral over S. Then the minimal polynomial minpoly S x either has natDegree at least 2 or x belongs to S; equivalently, 2 ≤ minpoly S x natDegree iff x ∉ S.

Русский

Пусть S — подполная алгебра B и x интегрирован над S. Тогда minpoly S x либо имеет natDegree ≥ 2, либо x принадлежит S; эквивалентно 2 ≤ (minpoly S x).natDegree тогда и только если x ∉ S.

LaTeX

$$$2 \le (\minpoly S x).natDegree \iff x \notin S$$$

Lean4

theorem two_le_natDegree_iff (int : IsIntegral A x) : 2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range :=
  by
  rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]
  exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩

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