isSeparable_adjoin_pair_of_isSeparable

English

Again, the same equivalence: Nat separable degree equals 1 iff there exists n with x^{q^n} in the base field image.

Русский

Снова та же эквивалентность: natSepDegree = 1 тогда и только тогда, существует n: x^{q^n} ∈ образ поля.

LaTeX

$$$ (minpoly F x).natSepDegree = 1 \iff \exists n : \mathbb{N}, x^{q^{n}} \in (algebraMap F E).range $$$

Lean4

/-- If `x` and `y` are both separable elements, then `F⟮x, y⟯ / F` is a separable extension.
As a consequence, any rational function of `x` and `y` is also a separable element. -/
theorem isSeparable_adjoin_pair_of_isSeparable {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) :
    Algebra.IsSeparable F F⟮x, y⟯ := by
  rw [← adjoin_simple_adjoin_simple]
  replace hy := IsSeparable.tower_top F⟮x⟯ hy
  rw [← isSeparable_adjoin_simple_iff_isSeparable] at hx hy
  exact Algebra.IsSeparable.trans F F⟮x⟯ F⟮x⟯⟮y⟯

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