Structures · Algebra
ExpChar
The definition of the exponential characteristic of a semiring.
- Defined in
- Mathlib.Algebra.CharP.Defs
- Shape
- 2 explicit arguments, not a structure
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- Polynomial
- RatFunc
- Polynomial.SplittingField
- AdjoinPthRoots
- MvPolynomial
- Subtype
- Prod
- LinearMap
How is a type an instance?
Loading the hierarchy index…
Assumed by289
- frobenius
- frobeniusEquiv
- iterateFrobenius
- iterateFrobeniusEquiv
- PerfectRing.lift
- ringExpChar.eq
- IsPerfectClosure
- IsPerfectClosure.equiv
- isPurelyInseparable_iff_pow_mem
- frobenius_def
- expChar_pow_pos
- expChar_of_injective_ringHom
- expChar_of_injective_algebraMap
- iterateFrobenius_one
- PerfectRing.liftEquiv
- iterateFrobenius_def
- frobenius_apply_frobeniusEquiv_symm
- PerfectRing.liftAux
- sub_pow_expChar_pow
- add_pow_expChar_pow_of_commute
- add_pow_expChar_of_commute
- add_pow_expChar
- frobenius_inj
- Polynomial.natSepDegree_expand
- IsPurelyInseparable.pow_mem
- sub_pow_expChar_pow_of_commute
- expChar_ne_zero
- frobeniusEquiv_apply
- PerfectRing.liftAux_self_apply
- IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable
- Irreducible.hasSeparableContraction
- minpoly.natSepDegree_eq_one_iff_pow_mem
- iterateFrobenius_inj
- iterateFrobeniusEquiv_add_apply
- PerfectRing.lift_comp_apply
- minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C
- frobeniusEquiv_symm_apply_frobenius
- IsPRadical.injective_comp_of_perfect
- iterateFrobenius_add
- Irreducible.natSepDegree_eq_one_iff_of_monic'
- IsPurelyInseparable.iterateFrobeniusₛₗ
- Polynomial.natSepDegree_X_pow_char_pow_sub_C
- expChar_pos
- PerfectRing.liftAux_id_apply
- iterate_frobenius
- expChar_is_prime_or_one
- Polynomial.roots_expand_pow
- sub_pow_expChar_of_commute
- iterateFrobenius_zero
- PerfectRing.lift_comp
Ancestors0
No ancestors.