Theorems · Definition · field theory

algebraicClosure.algEquivOfAlgEquiv

{F : Type u_1} →
  {E : Type u_2} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type u_3} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(algebraicClosure F E) ≃ₐ[F] ↥(algebraicClosure F K)

If E and K are isomorphic as F-algebras, then algebraicClosure F E and algebraicClosure F K are also isomorphic as F-algebras.

Defined in

Mathlib.FieldTheory.AlgebraicClosure

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra