Structures · Algebra
Normal
Typeclass for normal field extensions: an algebraic extension of fields K/F is normal
if the minimal polynomial of every element x in K splits in K, i.e. every F-conjugate
of x is in K.
- Defined in
- Mathlib.FieldTheory.Normal.Defs
- Shape
- 2 explicit arguments · adds splits'
Extends1
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by97
- AlgEquiv.restrictNormalHom
- AlgEquiv.restrictNormal_commutes
- AlgEquiv.restrictNormal
- AlgHom.restrictNormal_commutes
- AlgEquiv.liftNormal
- AlgEquiv.restrictNormalHom_surjective
- AlgHom.restrictNormal'
- Normal.algHomEquivAut
- AlgEquiv.restrictNormalHom_apply
- Normal.of_algEquiv
- AlgHom.restrictNormal
- spectralAlgNorm_of_finiteDimensional_normal
- IntermediateField.normal_iff_normalClosure_le
- AlgEquiv.liftNormal_commutes
- spectralNorm_eq_invariantExtension
- IntermediateField.normalClosure_def'
- spectralAlgNorm_of_finiteDimensional_normal_def
- AlgHom.liftNormal_commutes
- AlgHom.liftNormal
- IntermediateField.restrictRestrictAlgEquivMapHom
- Polynomial.Gal.restrict_surjective
- IntermediateField.normalClosureOperator
- IntermediateField.normalClosure_def''
- AlgHom.restrictNormalAux
- Normal.splits'
- AlgHom.fieldRange_of_normal
- IntermediateField.normal_iff_forall_map_le
- IsScalarTower.AlgEquiv.restrictNormalHom_comp
- spectralNorm_eq_iSup_of_finiteDimensional_normal
- isConjRoot_iff_exists_algEquiv
- InfiniteGalois.restrict_fixedField
- AlgHom.normal_bijective
- IntermediateField.normalClosure_of_normal
- IntermediateField.restrictRestrictAlgEquivMapHom_apply
- IntermediateField.normal_iff_forall_map_eq
- AlgEquiv.restrict_liftNormal
- AlgEquiv.restrictNormalHom_id
- Normal.of_equiv_equiv
- InfiniteGalois.restrictNormalHom_continuous
- normalClosure_eq_iSup_adjoin'
- AlgEquiv.restrictNormal_trans
- IntermediateField.normal_iff_normalClosure_eq
- IntermediateField.normal_iff_forall_map_le'
- AlgEquiv.restrictNormal_apply
- isNonarchimedean_spectralNorm_of_finiteDimensional_normal
- IntermediateField.map_fixingSubgroup
- IntermediateField.normal_iff_forall_fieldRange_le
- IntermediateField.map_fixingSubgroup_index
- IntermediateField.normal_iff_forall_fieldRange_eq
- minpoly.exists_algEquiv_of_root'