instIsAlgClosure — Mathlib

English

There is an IsAlgClosure structure on AlgebraicClosure(k), i.e., AlgebraicClosure(k) is an algebraic closure of k.

Русский

У AlgebraicClosure(k) есть структура IsAlgClosure, т.е. она является алгебраическим замыканием k.

LaTeX

$$$\text{IsAlgClosure } k (\text{AlgebraicClosure}(k)).$$$

Lean4

instance : IsAlgClosure k (AlgebraicClosure k) :=
  .of_splits fun f hf _ ↦
    by
    rw [show f = (⟨f, hf⟩ : Monics k) from rfl, ← splits_id_iff_splits, Monics.map_eq_prod]
    exact splits_prod _ fun _ _ ↦ (splits_id_iff_splits _).mpr (splits_X_sub_C _)

Похожие утверждения