Structures · Algebra
Polynomial.IsSplittingField
Typeclass characterising splitting fields.
- Shape
- 3 explicit arguments · adds splits', adjoin_rootSet'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- ZMod
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- Polynomial.IsSplittingField.splits
- Polynomial.IsSplittingField.adjoin_rootSet
- autEquivZmod
- adjoinRootXPowSubCEquiv
- autEquivRootsOfUnity
- rootOfSplitsXPowSubC
- IsGalois.of_separable_splitting_field
- Polynomial.IsSplittingField.finiteDimensional
- rootOfSplitsXPowSubC_pow
- isGalois_of_isSplittingField_X_pow_sub_C
- adjoinRootXPowSubCEquiv_symm_eq_root
- adjoinRootXPowSubCEquiv_root
- Polynomial.IsSplittingField.adjoin_rootSet'
- Polynomial.IsSplittingField.splits'
- Polynomial.IsSplittingField.IsScalarTower.splits
- Polynomial.IsSplittingField.lift
- spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots
- Algebra.adjoin_root_eq_top_of_isSplittingField
- autEquivRootsOfUnity_smul
- Polynomial.IsSplittingField.IsScalarTower.isAlgebraic
- Polynomial.IsSplittingField.adjoin_rootSet_eq_range
- isCyclic_of_isSplittingField_X_pow_sub_C
- autEquivRootsOfUnity_apply_rootOfSplit
- Polynomial.IsSplittingField.algEquiv
- autEquivZmod_symm_apply_intCast
- Normal.of_isSplittingField
- autEquivZmod_symm_apply_natCast
- IsGalois.of_separable_splitting_field_aux
- Polynomial.IsSplittingField.splits_iff
- rootOfSplitsXPowSubC.congr_simp
- adjoinRootXPowSubCEquiv.congr_simp
- Polynomial.IsSplittingField.map
- IntermediateField.adjoin_root_eq_top_of_isSplittingField
- Polynomial.IsSplittingField.of_algEquiv
- Algebra.isSeparable_of_separable_splitting_field
- Polynomial.IsSplittingField.mul
- autEquivRootsOfUnity.congr_simp
- autEquivZmod.congr_simp
- finrank_of_isSplittingField_X_pow_sub_C
Ancestors0
No ancestors.