Theorems · Definition · field theory

AlgEquiv.separableClosure

{F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {K : Type w} →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → (E ≃ₐ[F] K) → ↥(separableClosure F E) ≃ₐ[F] ↥(separableClosure F K)

Alias of separableClosure.algEquivOfAlgEquiv. If E and K are isomorphic as F-algebras, then separableClosure F E and separableClosure F K are also isomorphic as F-algebras.

Defined in

Mathlib.FieldTheory.SeparableClosure

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra