English
Every element of the algebraic closure AlgebraicClosure(k) is algebraic over k; i.e., AlgebraicClosure(k) is an algebraic extension of k.
Русский
Каждый элемент AlgebraicClosure(k) алгебраически зависим над k.
LaTeX
$$$\text{IsAlgebraic } k (\text{AlgebraicClosure}(k)).$$$
Lean4
instance isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) :=
⟨fun z =>
IsIntegral.isAlgebraic <| by
let ⟨p, hp⟩ := Ideal.Quotient.mk_surjective z
rw [← hp]
induction p using MvPolynomial.induction_on generalizing z with
| C => exact isIntegral_algebraMap
| add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl)
| mul_X p fi ih =>
rw [map_mul]
refine (ih _ rfl).mul ⟨_, fi.1.2, ?_⟩
simp_rw [← eval_map, Monics.map_eq_prod, eval_prod, Polynomial.map_sub, eval_sub]
apply Finset.prod_eq_zero (Finset.mem_univ fi.2)
rw [map_C]
-- The `erw` is needed here because the `R` in `eval` is `AlgebraicClosure k`,
-- but this has been unfolded in the arguments of `eval`.
erw [eval_C]
simp⟩
