Theorems · Inductive type · field theory
FiniteGaloisIntermediateField
(k : Type u_1) → (K : Type u_2) → [inst : Field k] → [inst_1 : Field K] → [Algebra k K] → Type u_2
The type of intermediate fields of K/k that are finite and Galois over k
- Defined in
- Mathlib.FieldTheory.Galois.GaloisClosure
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by50
Results whose statement or proof uses this declaration.
- FiniteGaloisIntermediateField.toIntermediateFieldstatement and proof · cited by 25
- InfiniteGalois.asProfiniteGaloisGroupFunctorstatement · cited by 13
- FiniteGaloisIntermediateField.adjoinstatement · cited by 11
- InfiniteGalois.projstatement and proof · cited by 6
- InfiniteGalois.limitToAlgEquivstatement · cited by 3
- InfiniteGalois.mulEquivToLimitstatement · cited by 3
- FiniteGaloisIntermediateField.adjoin_simple_le_iffstatement and proof · cited by 3
- finGaloisGroupFunctorstatement and proof · cited by 2
- finGaloisGroupMapstatement and proof · cited by 2
- InfiniteGalois.toAlgEquivAux_eq_proj_of_memstatement and proof · cited by 2
- FiniteGaloisIntermediateField.finGaloisGroupstatement and proof · cited by 2
- InfiniteGalois.algEquivToLimitstatement and proof · cited by 1