Structures · Algebra
IsGalois
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
- Shape
- 2 explicit arguments · adds to_isSeparable, to_normal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every IsGalois is also a
Concrete types that are instances2
- FractionRing
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by137
- IsGalois.card_aut_eq_finrank
- FiniteGaloisIntermediateField.adjoin
- IsGalois.intermediateFieldEquivSubgroup
- Algebra.norm_eq_prod_automorphisms
- NumberField.InfinitePlace.isUnramifiedIn_comap
- IsGalois.tower_top_of_isGalois
- IsGalois.of_algEquiv
- FiniteGaloisIntermediateField.adjoin_simple_le_iff
- InfiniteGalois.mulEquivToLimit
- NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two
- InfiniteGalois.fixedField_fixingSubgroup
- InfiniteGalois.limitToAlgEquiv
- IsGalois.intermediateFieldEquivSubgroup_apply
- NumberField.InfinitePlace.even_card_aut_of_not_isUnramified
- NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one
- IntermediateField.LinearDisjoint.of_inf_eq_bot
- NumberField.InfinitePlace.mem_orbit_iff
- IsGalois.is_separable_splitting_field
- IsGalois.integral
- InfiniteGalois.toAlgEquivAux_eq_proj_of_mem
- IsGalois.fixedField_top
- NumberField.InfinitePlace.even_finrank_of_not_isUnramified
- IsGalois.splits
- IsGalois.separable
- NumberField.InfinitePlace.card_stabilizer
- IsGalois.fixedField_fixingSubgroup
- InfiniteGalois.normal_iff_isGalois
- IsGalois.mem_bot_iff_fixed
- NumberField.InfinitePlace.exists_smul_eq_of_comap_eq
- NumberField.InfinitePlace.orbitRelEquiv
- InfiniteGalois.IntermediateFieldEquivClosedSubgroup
- NumberField.InfinitePlace.card_eq_card_isUnramifiedIn
- NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
- trace_eq_sum_automorphisms
- IsGalois.normalAutEquivQuotient
- groupCohomology.norm_ofAlgebraAutOnUnits_eq
- IsInertiaField.rank_right
- RingOfIntegers.dvd_norm
- NumberField.linearDisjoint_of_isGalois_isCoprime_discr
- NumberField.InfinitePlace.card_isUnramified_compl
- Ideal.relNorm_eq_pow_of_isPrime_isGalois
- InfiniteGalois.proj_adjoin_singleton_val
- prod_galRestrict_eq_norm
- groupCohomology.exists_div_of_norm_eq_one
- NumberField.InfinitePlace.exists_isConj_of_isRamified
- exists_root_adjoin_eq_top_of_isCyclic
- InfiniteGalois.mem_bot_iff_fixed
- IsGalois.normalBasis
- Algebra.algebraMap_intNorm_of_isGalois
- IsGalois.card_fixingSubgroup_eq_finrank