Structures · Algebra
IsPurelyInseparable.HasExponent
A predicate class on a ring extension saying that there is a natural number e
such that a ^ ringExpChar K ^ e ∈ K for all a ∈ L.
- Shape
- 2 explicit arguments · adds has_exponent
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- IsPurelyInseparable.exponent
- IsPurelyInseparable.iterateFrobeniusₛₗ
- IsPurelyInseparable.HasExponent.has_exponent
- IsPurelyInseparable.algebraMap_iterateFrobenius
- IsPurelyInseparable.iterateFrobenius
- IsPurelyInseparable.exponent_def
- IsPurelyInseparable.iterateFrobenius_algebraMap
- IsPurelyInseparable.exponent_min
- IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ
- IsPurelyInseparable.elemExponent_le_exponent
- IsPurelyInseparable.exponent_min'
- IsPurelyInseparable.exponent_def'
- IsPurelyInseparable.instOfHasExponent
- IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap
- IsPurelyInseparable.iterateFrobeniusₛₗ_algebraMap_base
Ancestors0
No ancestors.