Theorems · Inductive type · field theory
IsGalois
(F : Type u_1) → [inst : Field F] → (E : Type u_2) → [inst_1 : Field E] → [Algebra F E] → Prop
A field extension E/F is Galois if it is both separable and normal. Note that in mathlib a separable extension of fields is by definition algebraic.
- Defined in
- Mathlib.FieldTheory.Galois.Basic
- Cited by
- 149 results in Mathlib
- Foundations
- Depth 45 from the axioms, rests on 389 definitions · 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 by174
Results whose statement or proof uses this declaration.
- IsGalois.card_aut_eq_finrankstatement and proof · cited by 16
- IsCyclotomicExtension.isGaloisstatement · cited by 13
- FiniteGaloisIntermediateField.adjoinstatement and proof · cited by 11
- IsGalois.intermediateFieldEquivSubgroupstatement and proof · cited by 10
- IsGaloisGroup.intermediateFieldEquivSubgroupproof · cited by 6
- Algebra.norm_eq_prod_automorphismsstatement and proof · cited by 5
- NumberField.InfinitePlace.isUnramifiedIn_comapstatement and proof · cited by 4
- IsGalois.tower_top_of_isGaloisstatement and proof · cited by 4
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomicproof · cited by 3
- InfiniteGalois.fixedField_fixingSubgroupstatement and proof · cited by 3
- InfiniteGalois.limitToAlgEquivstatement and proof · cited by 3