Theorems · Theorem · field theory

AlgHom.restrictNormal.congr_simp

∀ {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₂] (ϕ ϕ_1 : K₁ →ₐ[F] K₂),
  ϕ = ϕ_1 →
    ∀ (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₂] [inst_11 : Normal F E],
      ϕ.restrictNormal E = ϕ_1.restrictNormal E

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraFieldAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerNormal