instIsAlgClosureOfIsAlgebraic — Mathlib

English

If L is a field extension of k with L algebraic over k, then IsAlgClosure k (AlgebraicClosure L) holds.

Русский

Если L является полем-наслоение над k и L алгебраическое над k, тогда IsAlgClosure k (AlgebraicClosure L) выполняется.

LaTeX

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

Lean4

instance {L : Type*} [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L] : IsAlgClosure k (AlgebraicClosure L)
    where
  isAlgebraic := .trans k L _
  isAlgClosed := inferInstance

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