Structures · Algebra
IsAbelianGalois
The class of abelian extensions, defined as galois extensions whose galois group is commutative.
- Defined in
- Mathlib.FieldTheory.Galois.Abelian
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar
- IsAbelianGalois.tower_bot
- NumberField.IsCMField.of_isAbelianGalois
- IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar.congr_simp
- IsAbelianGalois.tower_top
- IsAbelianGalois.toIsMulCommutative
- IsAbelianGalois.of_algHom
- instIsAbelianGaloisSubtypeMemIntermediateField_1
- IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff_conductor_dvd
- IsAbelianGalois.toIsGalois
- IsCyclotomicExtension.Rat.card_intermediateFieldEquivSubgroupChar
- IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff
- instIsAbelianGaloisSubtypeMemIntermediateField