isConjRoot_iff_exists_algEquiv — Mathlib

English

If y is a conjugate root over L of x, then y is a conjugate root over K of x in a tower K ⊂ L ⊂ S.

Русский

Если y сопряжён над L к x, то он сопряжён над K к x в башне K ⊂ L ⊂ S.

LaTeX

$$$IsConjRoot(K, x, y) \Rightarrow IsConjRoot(K, x, y) \quad\text{given } IsScalarTower(K, L, S)$$$

Lean4

/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, `y` is a
conjugate root of `x` if and only if there exists a `K`-automorphism `σ : L ≃ₐ[K] L` such
that `σ y = x`.
-/
theorem isConjRoot_iff_exists_algEquiv [Normal K L] {x y : L} : IsConjRoot K x y ↔ ∃ σ : L ≃ₐ[K] L, σ y = x :=
  ⟨exists_algEquiv, fun ⟨_, h⟩ => h ▸ (isConjRoot_of_algEquiv _ _).symm⟩

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