English
The map sending the generator of K⟮x⟯ to the generator of K⟮y⟯ under a minpoly equality is the algebra isomorphism.
Русский
Отображение, переводящее генератор K⟮x⟯ в генератор K⟮y⟯ при равенстве minpoly, является изоморфизмом алгебр.
LaTeX
$$minpoly.algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y$$
Lean4
/-- `minpoly.algEquiv` sends the generator of `K⟮x⟯` to the generator of `K⟮y⟯`. -/
theorem algEquiv_apply {x y : L} (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y) :
algEquiv hx h_mp (AdjoinSimple.gen K x) = AdjoinSimple.gen K y :=
by
have hy : IsAlgebraic K y := ⟨minpoly K x, ne_zero hx.isIntegral, (h_mp ▸ aeval _ _)⟩
rw [algEquiv, trans_apply, ← adjoinRootEquivAdjoin_apply_root K hx.isIntegral, symm_apply_apply, trans_apply,
AdjoinRoot.algEquivOfEq_root, adjoinRootEquivAdjoin_apply_root K hy.isIntegral]
