two_le_natDegree_subalgebra — Mathlib

English

In the Subalgebra setting, for an integral element x over S, 2 ≤ natDegree(minpoly S x) is equivalent to x ∉ S.

Русский

В настройке подполной алгебры для интеграла x над S, 2 ≤ natDegree(minpoly S x) эквивалентно x ∉ S.

LaTeX

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

Lean4

theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B] {S : Subalgebra A B} {x : B}
    (int : IsIntegral S x) : 2 ≤ (minpoly S x).natDegree ↔ x ∉ S :=
  by
  rw [two_le_natDegree_iff int, Iff.not]
  apply Set.ext_iff.mp Subtype.range_val_subtype

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