English
Under the same hypotheses as the previous result, there exists a K-algebra automorphism σ of L such that σ(y) = x, i.e., y is a Galois conjugate of x over K.
Русский
При тех же предположениях существует K-алгебраическая автоморфия σ:L→L такая, что σ(y)=x; то есть y является Галуа-сопряженным к x над K.
LaTeX
$$$\exists \sigma: L \simeq_K L, \ σ(y) = x$$$
Lean4
/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : L ≃ₐ[K] L)` with `σ y = x`.
That is, `x` and `y` are Galois conjugates. -/
theorem exists_algEquiv_of_root' [Normal K L] {x y : L} (hy : IsAlgebraic K y)
(h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ y = x :=
by
obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev
use σ.symm
rw [← hσ, symm_apply_apply]
