instIsAlgClosure — Mathlib

English

If k ≃+* k′ and k is algebraically closed, then k′ is algebraically closed.

Русский

Если существует эквиалентность колец k ≃+* k′ и k алгебраически замкнуто, то и k′ алгебраически замкнуто.

LaTeX

$$$\forall (k : Type u) [\mathrm{Field}\;k] (k' : Type u) [\mathrm{Field}\;k'] (e : k \simeq_+* k') [IsAlgClosed k], IsAlgClosed k'$$$

Lean4

instance instIsAlgClosure (F : Type*) [Field F] [IsAlgClosed F] : IsAlgClosure F F
    where
  isAlgClosed := ‹_›
  isAlgebraic := .of_finite F F

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