Theorems · Definition · field theory

AlgHom.restrictNormalAux

{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₂] →
                            [inst_9 : IsScalarTower F E K₁] →
                              [inst_10 : IsScalarTower F E K₂] →
                                [h : Normal F E] →
                                  ↥(IsScalarTower.toAlgHom F E K₁).range →ₐ[F] ↥(IsScalarTower.toAlgHom F E K₂).range

Restrict algebra homomorphism to image of normal subfield

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal