English
If k is a field and k' is ring-equivalent to k via e, and k is algebraically closed, then k' is algebraically closed.
Русский
Если k — поле и k' эквивалентно как кольцо через э, и k алгебраически замкнуто, то k' также алгебраически замкнуто.
LaTeX
$$$\forall (k : Type) [\mathrm{Field}\;k] (k' : Type) [\mathrm{Field}\;k'] (e : k \simeq_+* k') [IsAlgClosed k], IsAlgClosed k'$$$
Lean4
theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k') [IsAlgClosed k] : IsAlgClosed k' :=
by
apply IsAlgClosed.of_exists_root
intro p hmp hp
have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
rw [degree_map]
exact ne_of_gt (degree_pos_of_irreducible hp)
rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩
use e x
rw [IsRoot] at hx
apply e.symm.injective
rw [map_zero, ← hx]
clear hx hpe hp hmp
induction p using Polynomial.induction_on <;> simp_all
