Theorems · Theorem · field theory

IsAlgClosure.ofAlgebraic

∀ (K : Type u_1) (J : Type u_2) (L : Type v) [inst : Field K] [inst_1 : Field J] [inst_2 : Field L]
  [inst_3 : Algebra K J] [inst_4 : Algebra J L] [IsAlgClosure J L] [inst_6 : Algebra K L] [IsScalarTower K J L]
  [Algebra.IsAlgebraic K J], IsAlgClosure K L

If J is an algebraic extension of K and L is an algebraic closure of J, then it is also an algebraic closure of K.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Basic

Cited by

0 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldFieldAlgebraAlgebraIsAlgClosureAlgebraIsScalarTowerAlgebra.IsAlgebraic