Exponent

📁 Source: Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

Statistics

Metric	Count
Definitions HasExponent, elemExponent, elemReduct, exponent, iterateFrobenius, iterateFrobeniusₛₗ	6
Theorems has_exponent, algebraMap_elemReduct_eq, algebraMap_elemReduct_eq', algebraMap_iterateFrobenius, algebraMap_iterateFrobeniusₛₗ, elemExponent_def, elemExponent_def', elemExponent_eq_zero_of_charZero, elemExponent_eq_zero_of_mem_range, elemExponent_le_exponent, elemExponent_le_of_pow_mem, elemExponent_le_of_pow_mem', elemExponent_min, elemExponent_min', exponent_def, exponent_def', exponent_min, exponent_min', hasExponent_iff, hasExponent_iff', hasExponent_of_finiteDimensional, instOfHasExponent, iterateFrobenius_algebraMap, iterateFrobeniusₛₗ_algebraMap, iterateFrobeniusₛₗ_algebraMap_base, minpoly_eq, minpoly_eq', minpoly_natDegree_eq, minpoly_natDegree_eq'	29
Total	35

IsPurelyInseparable

Definitions

Name	Category	Theorems
HasExponent 📖	CompData	3 math math: hasExponent_iff, hasExponent_of_finiteDimensional, hasExponent_iff'
elemExponent 📖	CompOp	13 math math: minpoly_natDegree_eq', minpoly_eq', elemExponent_le_of_pow_mem, elemExponent_def', minpoly_eq, elemExponent_eq_zero_of_mem_range, minpoly_natDegree_eq, algebraMap_elemReduct_eq', elemExponent_le_exponent, elemExponent_eq_zero_of_charZero, algebraMap_elemReduct_eq, elemExponent_le_of_pow_mem', elemExponent_def
elemReduct 📖	CompOp	4 math math: minpoly_eq', minpoly_eq, algebraMap_elemReduct_eq', algebraMap_elemReduct_eq
exponent 📖	CompOp	3 math math: exponent_def', elemExponent_le_exponent, exponent_def
iterateFrobenius 📖	CompOp	2 math math: iterateFrobenius_algebraMap, algebraMap_iterateFrobenius
iterateFrobeniusₛₗ 📖	CompOp	3 math math: iterateFrobeniusₛₗ_algebraMap, iterateFrobeniusₛₗ_algebraMap_base, algebraMap_iterateFrobeniusₛₗ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_elemReduct_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap elemReduct Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar elemExponent	—	minpoly.aeval minpoly_eq sub_eq_zero Polynomial.aeval_X map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_C map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass
algebraMap_elemReduct_eq' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap elemReduct Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid elemExponent	—	algebraMap_elemReduct_eq ringExpChar.eq
algebraMap_iterateFrobenius 📖	mathematical	exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap iterateFrobenius Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	—
algebraMap_iterateFrobeniusₛₗ 📖	mathematical	exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap LinearMap iterateFrobenius NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule LinearMap.instFunLike iterateFrobeniusₛₗ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	algebraMap_iterateFrobenius
elemExponent_def 📖	mathematical	—	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring elemExponent	—	RingHom.mem_range algebraMap_elemReduct_eq
elemExponent_def' 📖	mathematical	—	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid elemExponent	—	elemExponent_def ringExpChar.eq
elemExponent_eq_zero_of_charZero 📖	mathematical	—	elemExponent	—	elemExponent_eq_zero_of_mem_range surjective_algebraMap_of_isSeparable Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic normal PerfectField.ofCharZero
elemExponent_eq_zero_of_mem_range 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	elemExponent	—	Nat.find_eq_zero pow_zero pow_one minpoly.eq_X_sub_C EuclideanDomain.toNontrivial
elemExponent_le_exponent 📖	mathematical	—	elemExponent exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	elemExponent_le_of_pow_mem exponent_def
elemExponent_le_of_pow_mem 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring	elemExponent	—	ExpChar.exists instIsDomain elemExponent_eq_zero_of_charZero RingHom.mem_range map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_C Polynomial.aeval_X_pow sub_eq_zero Polynomial.monic_X_pow_sub_C expChar_pow_pos ringExpChar.expChar Polynomial.natDegree_sub_C Polynomial.natDegree_pow IsDomain.to_noZeroDivisors Polynomial.natDegree_X EuclideanDomain.toNontrivial mul_one Nat.Prime.one_lt Polynomial.natDegree_le_natDegree minpoly.min minpoly_natDegree_eq ringExpChar.eq
elemExponent_le_of_pow_mem' 📖	mathematical	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	elemExponent	—	elemExponent_le_of_pow_mem ringExpChar.eq
elemExponent_min 📖	mathematical	elemExponent	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring	—	elemExponent_le_of_pow_mem
elemExponent_min' 📖	mathematical	elemExponent	Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	elemExponent_min ringExpChar.eq
exponent_def 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring CommSemiring.toSemiring exponent	—	Nat.find_spec HasExponent.has_exponent
exponent_def' 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid exponent	—	exponent_def ringExpChar.eq
exponent_min 📖	mathematical	exponent	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Nat.find_min HasExponent.has_exponent
exponent_min' 📖	mathematical	exponent	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	exponent_min ringExpChar.eq
hasExponent_iff 📖	mathematical	—	HasExponent Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
hasExponent_iff' 📖	mathematical	—	HasExponent Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	hasExponent_iff ringExpChar.eq
hasExponent_of_finiteDimensional 📖	mathematical	—	HasExponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	ExpChar.exists instIsDomain surjective_algebraMap_of_isSeparable Algebra.IsAlgebraic.isSeparable_of_perfectField Normal.toIsAlgebraic normal PerfectField.ofCharZero Nat.le_log_of_pow_le Nat.Prime.one_lt ringExpChar.eq minpoly.natDegree_le minpoly_natDegree_eq map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_elemReduct_eq pow_mul pow_add
instOfHasExponent 📖	mathematical	—	IsPurelyInseparable EuclideanDomain.toCommRing Field.toEuclideanDomain	—	HasExponent.has_exponent isPurelyInseparable_iff_pow_mem ringExpChar.expChar instIsDomain
iterateFrobenius_algebraMap 📖	mathematical	exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike iterateFrobenius CommSemiring.toSemiring Semifield.toCommSemiring algebraMap Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_iterateFrobenius
iterateFrobeniusₛₗ_algebraMap 📖	mathematical	exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield iterateFrobenius NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring LinearMap.instFunLike iterateFrobeniusₛₗ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	iterateFrobenius_algebraMap
iterateFrobeniusₛₗ_algebraMap_base 📖	mathematical	exponent EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield iterateFrobenius NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring LinearMap.instFunLike iterateFrobeniusₛₗ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	RingHom.injective DivisionRing.isSimpleRing EuclideanDomain.toNontrivial map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.algebraMap_apply algebraMap_iterateFrobeniusₛₗ
minpoly_eq 📖	mathematical	—	minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring elemExponent DFunLike.coe RingHom RingHom.instFunLike Polynomial.C elemReduct	—	minpoly_eq_X_pow_sub_C ringExpChar.expChar instIsDomain Nat.find_spec
minpoly_eq' 📖	mathematical	—	minpoly EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.instMonoid elemExponent DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C elemReduct	—	minpoly_eq ringExpChar.eq
minpoly_natDegree_eq 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield elemExponent	—	minpoly_eq Polynomial.natDegree_sub_C Polynomial.natDegree_pow IsDomain.to_noZeroDivisors instIsDomain Polynomial.natDegree_X EuclideanDomain.toNontrivial mul_one
minpoly_natDegree_eq' 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain minpoly DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow Nat.instMonoid elemExponent	—	minpoly_natDegree_eq ringExpChar.eq

IsPurelyInseparable.HasExponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_exponent 📖	mathematical	—	Subring SetLike.instMembership Subring.instSetLike RingHom.range CommRing.toRing algebraMap CommRing.toCommSemiring Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid ringExpChar Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—

---

← Back to Index