Mathlib Map

Theorems · Theorem · field theory

IsGalois.tower_top_of_isGalois

∀ (F : Type u_1) (K : Type u_2) (E : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field E]
  [inst_3 : Algebra F K] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [IsScalarTower F K E] [IsGalois F E],
  IsGalois K E

Let $E / K / F$ be a tower of field extensions. If $E$ is Galois over $F$, then $E$ is Galois over $K$.

Defined in
Mathlib.FieldTheory.Galois.Basic
Cited by
4 results in Mathlib
Foundations
Depth 142 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFieldFieldAlgebraAlgebraAlgebraIsScalarTowerIsGalois
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isGalois_iff_isGalois_bot · cited by 2isGalois_iff_isGalois_botRingOfIntegers.isUnit_norm · cited by 1RingOfIntegers.isUnit_normIdeal.relNorm_eq_pow_of_isMaximal · cited by 1Ideal.relNorm_eq_pow_of_i…IsAbelianGalois.tower_top · cited by 0IsAbelianGalois.tower_topAlgebra · cited by 11388AlgebraField · cited by 7404FieldIsScalarTower · cited by 3896IsScalarTowerIsGalois · cited by 149IsGaloisIsGalois.tower_top_of_isGaloisCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Algebrastatement and proof · cited by 11,388
  • Fieldstatement and proof · cited by 7,404
  • IsScalarTowerstatement and proof · cited by 3,896
  • IsGaloisstatement and proof · cited by 149

Cited by4

Results whose statement or proof uses this declaration.