isAlgClosure_iff — Mathlib

English

For field k and extension K, IsAlgClosure k K holds if and only if IsAlgClosed K and Algebra.IsAlgebraic k K.

Русский

Для поля k и расширения K условие IsAlgClosure k K эквивалентно IsAlgClosed K и Algebra.IsAlgebraic k K.

LaTeX

$$$\forall (k : Type u) [\mathrm{Field}\;k] (K : Type v) [\mathrm{Field}\;K] [\mathrm{Algebra}\;k K], IsAlgClosure k K \iff (IsAlgClosed K \wedge Algebra.IsAlgebraic k K)$$$

Lean4

theorem isAlgClosure_iff (K : Type v) [Field K] [Algebra k K] :
    IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K :=
  ⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩

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