English
If x and y have the same minimal polynomial over K and are algebraic over K, then the canonical algEquiv between K⟮x⟯ and K⟮y⟯ sends the generator x to the generator y.
Русский
Пусть x и y над K имеют одинаковый минимальный полином; тогда каноническое алгебравариантное соответствие между K⟮x⟯ и K⟮y⟯ отправляет генератор x в генератор y.
LaTeX
$$minpoly.algEquiv hx h_mp sends AdjoinSimple.gen K x to AdjoinSimple.gen K y$$
Lean4
/-- The canonical `algEquiv` between `K⟮x⟯`and `K⟮y⟯`, sending `x` to `y`, where `x` and `y` have
the same minimal polynomial over `K`. -/
noncomputable def algEquiv {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) : K⟮x⟯ ≃ₐ[K] K⟮y⟯ :=
by
have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
exact
AlgEquiv.trans (adjoinRootEquivAdjoin K hx.isIntegral).symm
(AlgEquiv.trans (AdjoinRoot.algEquivOfEq _ _ h_mp) (adjoinRootEquivAdjoin K hy.isIntegral))
