English
If the ranges of minpoly for E and K are equal, there exists a K-algebra isomorphism between E and K.
Русский
Если диапазоны minpoly у E и K совпадают, существует K-алгебрический эквивалент между E и K.
LaTeX
$$$\\text{range}(minpoly\\ F|_E) = \\text{range}(minpoly\\ F|_K) \\Rightarrow \\exists \\sigma: E \\simeq_F K$$$
Lean4
theorem nonempty_algEquiv_of_range_minpoly_eq (h : Set.range (@minpoly F E _ _ _) = Set.range (@minpoly F K _ _ _)) :
Nonempty (E ≃ₐ[F] K) :=
have ⟨σ⟩ := nonempty_algHom_of_range_minpoly_subset h.le
have : Algebra.IsAlgebraic F K :=
⟨fun y ↦
IsIntegral.isAlgebraic <| by
by_contra hy
have ⟨x, hx⟩ := h.ge ⟨y, rfl⟩
rw [minpoly.eq_zero hy] at hx
exact minpoly.ne_zero ((alg.isIntegral).1 x) hx⟩
have ⟨τ⟩ := nonempty_algHom_of_range_minpoly_subset h.ge
⟨.ofBijective _ (Algebra.IsAlgebraic.algHom_bijective₂ σ τ).1⟩
