natDegree_eq_one_iff — Mathlib

English

For x integral over A, the natDegree of minpoly A x equals 1 if and only if x lies in the image of the base algebra map A → B.

Русский

Для x, интегрированного над A, natDegree(minpoly A x) равно 1 тогда и только тогда, когда x лежит в образе алгебраического отображения A → B.

LaTeX

$$$(\minpoly A x).natDegree = 1 \iff x \in (\operatorname{algebraMap} A B).range$$$

Lean4

theorem natDegree_eq_one_iff : (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range :=
  by
  rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one]
  exact degree_eq_one_iff

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