Structures · Algebra
IsGaloisGroup
G is a Galois group for L/K if the action of G on L is faithful with fixed field K.
In particular, we do not assume that L is an algebraic extension of K.
See the implementation notes in this file for the meaning of this definition in the case of rings.
- Defined in
- Mathlib.RingTheory.IsGaloisGroup.Defs
- Shape
- 3 explicit arguments · adds faithful, commutes, isInvariant
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every IsGaloisGroup is also a
Concrete types that are instances3
- AlgEquiv
- Subtype
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by113
- Ideal.inertiaDegIn_eq_inertiaDeg
- Ideal.ramificationIdxIn_eq_ramificationIdx
- IsGaloisGroup.card_eq_finrank
- IsGaloisGroup.mulEquivAlgEquiv
- IsGaloisGroup.ringEquivFixedPoints
- Ideal.exists_smul_eq_of_isGaloisGroup
- IsGaloisGroup.faithful
- IsGaloisGroup.ringEquivFixedPoints_apply_coe
- IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply
- IsGaloisGroup.intermediateFieldEquivSubgroup
- IsGaloisGroup.mulEquivCongr
- IsGaloisGroup.restrictHom
- IsGaloisGroup.of_isFractionRing
- Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn
- IsGaloisGroup.fixedPoints_eq_bot
- IsGaloisGroup.quotientMulEquiv
- IsGaloisGroup.mulEquivAlgEquiv_apply_apply
- IsGaloisGroup.of_mulEquiv
- IsGaloisGroup.mulEquivCongr_apply_smul
- IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply
- Ideal.card_inertia_eq_ramificationIdxIn
- IsGaloisGroup.smulOfNormal
- IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply
- IsGaloisGroup.ringEquiv
- Ideal.card_stabilizer_eq
- Ideal.card_stabilizer_eq_card_inertia_mul_finrank
- IsGaloisGroup.to_isFractionRing_of_isIntegral
- Ideal.inertiaDeg_eq_of_isGaloisGroup
- IsGaloisGroup.fixingSubgroup_fixedPoints
- IsGaloisGroup.mulSemiringActionOfNormal
- IsGaloisGroup.smul_mem_of_normal
- IsGaloisGroup.card_eq_finrank'
- IsGaloisGroup.algebraMap_smulOfNormal
- IsGaloisGroup.mulSemiringActionQuotient
- Ideal.ncard_primesOver_mul_card_inertia_mul_finrank
- IsGaloisGroup.fixedPoints_eq_range_algebraMap
- Ideal.ramificationIdxIn_ne_zero
- IsGaloisGroup.algebraMap_restrictHom_smul
- IsGaloisGroup.of_ringHom_surjective
- IsGaloisGroup.quotient
- IsGaloisGroup.algebraMap_quotientMulEquiv_smul
- IsInertiaField.rank_right
- IsGaloisGroup.fixedPoints_of_isGaloisGroup
- IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup
- IsGaloisGroup.restrictHom_smul_under
- Ideal.ramificationIdxIn_mul_ramificationIdxIn
- IsGaloisGroup.isGalois
- IsGaloisGroup.of_ringEquiv
- IsGaloisGroup.fixingSubgroup_range_algebraMap
- IsGaloisGroup.mulEquivCongr_symm_apply_smul