Structures · Algebra
IsPurelyInseparable
Typeclass for purely inseparable field extensions: an algebraic extension E / F is purely
inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable.
We define this for general (commutative) rings and only assume F and E are fields
if this is needed for a proof.
- Shape
- 2 explicit arguments · adds isIntegral, inseparable'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every IsPurelyInseparable is also a
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by73
- IsPurelyInseparable.elemExponent
- IsPurelyInseparable.surjective_algebraMap_of_isSeparable
- IsPurelyInseparable.elemReduct
- IsPurelyInseparable.inseparable
- IsPurelyInseparable.pow_mem
- IsPurelyInseparable.inseparable'
- IsPurelyInseparable.tower_top
- IsPurelyInseparable.minpoly_eq
- IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable
- IsPurelyInseparable.injective_comp_algebraMap
- IsPurelyInseparable.isIntegral'
- IsPurelyInseparable.elemExponent_le_of_pow_mem
- separableClosure.eq_bot_of_isPurelyInseparable
- IsPurelyInseparable.algebraMap_elemReduct_eq
- separableClosure_le
- IsPurelyInseparable.finrank_eq_pow
- IsPurelyInseparable.minpoly_eq_X_pow_sub_C
- IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable
- Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable
- IntermediateField.linearDisjoint_of_isPurelyInseparable_of_isSeparable
- IsPurelyInseparable.finSepDegree_eq_one
- IsPurelyInseparable.minpoly_natDegree_eq
- IsPurelyInseparable.elemExponent_eq_zero_of_mem_range
- IsPurelyInseparable.elemExponent_min
- IsPurelyInseparable.sepDegree_eq_one
- eq_separableClosure
- Field.sepDegree_eq_of_isPurelyInseparable
- Algebra.FormallyUnramified.range_eq_top_of_isPurelyInseparable
- LinearIndependent.map_of_isPurelyInseparable_of_isSeparable
- IsPurelyInseparable.injective_restrictDomain
- Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable
- IsPurelyInseparable.elemExponent_def
- IsPurelyInseparable.elemExponent_eq_zero_of_charZero
- le_perfectClosure
- IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar
- minpoly.map_eq_of_isSeparable_of_isPurelyInseparable
- PrimeSpectrum.isHomeomorph_comap_of_isPurelyInseparable
- IsPurelyInseparable.tower_bot
- IsPurelyInseparable.trans
- IsPurelyInseparable.exists_pow_mem_range_tensorProduct
- IsPurelyInseparable.insepDegree_eq
- AlgEquiv.isPurelyInseparable
- IsPurelyInseparable.elemExponent_le_exponent
- IntermediateField.isPurelyInseparable_sup
- Polynomial.Separable.map_irreducible_of_isPurelyInseparable
- IsPurelyInseparable.elemExponent_le_of_pow_mem'
- IsPurelyInseparable.finInsepDegree_eq
- IntermediateField.isPurelyInseparable_tower_bot
- IsPurelyInseparable.elemExponent_def'
- IsPurelyInseparable.bijective_comp_algebraMap