Theorems · Definition · field theory

AlgEquiv.restrictNormal

{F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ ≃ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra E K₁] →
                          [inst_8 : Algebra E K₂] →
                            [IsScalarTower F E K₁] → [IsScalarTower F E K₂] → [Normal F E] → Gal(E/F)

Restrict algebra isomorphism to a normal subfield

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

12 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal