Perfect

📁 Source: Mathlib/FieldTheory/Perfect.lean

Statistics

Metric	Count
Definitions PerfectField, PerfectRing, rootsExpandEquivRoots, rootsExpandPowEquivRoots, rootsExpandPowToRoots, rootsExpandToRoots, frobeniusEquiv, iterateFrobeniusEquiv	8
Theorems isSeparable_of_perfectField, perfectField, map_frobeniusEquiv_symm, map_iterate_frobeniusEquiv_symm, ofCharZero, ofFinite, separable_iff_squarefree, separable_of_irreducible, toPerfectRing, bijective_frobenius, ofFiniteOfIsReduced, ofSurjective, toPerfectField, rootsExpandEquivRoots_apply, rootsExpandPowEquivRoots_apply, rootsExpandPowToRoots_apply, rootsExpandToRoots_apply, roots_X_pow_char_pow_sub_C, roots_X_pow_char_pow_sub_C_pow, roots_X_pow_char_sub_C, roots_X_pow_char_sub_C_pow, roots_expand, roots_expand_image_frobenius, roots_expand_image_frobenius_subset, roots_expand_image_iterateFrobenius, roots_expand_map_frobenius, roots_expand_map_frobenius_le, roots_expand_pow, roots_expand_pow_image_iterateFrobenius_subset, roots_expand_pow_map_iterateFrobenius, roots_expand_pow_map_iterateFrobenius_le, map_frobeniusEquiv_symm, map_iterate_frobeniusEquiv_symm, bijective_frobenius, bijective_iterateFrobenius, coe_frobeniusEquiv, coe_frobeniusEquiv_symm_comp_coe_frobenius, coe_frobenius_comp_coe_frobeniusEquiv_symm, coe_iterateFrobeniusEquiv, frobeniusEquiv_apply, frobeniusEquiv_def, frobeniusEquiv_symm_apply_frobenius, frobeniusEquiv_symm_comp_frobenius, frobeniusEquiv_symm_pow, frobeniusEquiv_symm_pow_p, frobenius_apply_frobeniusEquiv_symm, frobenius_comp_frobeniusEquiv_symm, injective_frobenius, injective_pow_p, instPerfectRingProd, iterateFrobeniusEquiv_add, iterateFrobeniusEquiv_add_apply, iterateFrobeniusEquiv_apply, iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_eq_pow, iterateFrobeniusEquiv_one, iterateFrobeniusEquiv_one_apply, iterateFrobeniusEquiv_symm, iterateFrobeniusEquiv_symm_add, iterateFrobeniusEquiv_symm_add_apply, iterateFrobeniusEquiv_zero, iterateFrobeniusEquiv_zero_apply, iterate_frobeniusEquiv_symm_pow_p_pow, not_irreducible_expand, polynomial_expand_eq, surjective_frobenius	66
Total	74

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparable_of_perfectField 📖	mathematical	—	Algebra.IsSeparable EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	PerfectField.separable_of_irreducible minpoly.irreducible instIsDomain Algebra.IsIntegral.isIntegral isIntegral
perfectField 📖	mathematical	—	PerfectField	—	Irreducible.exists_dvd_monic_irreducible_of_isIntegral instIsDomain isIntegral Polynomial.Separable.of_dvd Polynomial.Separable.map PerfectField.separable_of_irreducible

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring instFunLike RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	Equiv.injective frobenius_apply_frobeniusEquiv_symm RingEquiv.apply_symm_apply
map_iterate_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring instFunLike Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	Function.Injective.iterate Function.Commute.comp_iterate coe_frobeniusEquiv RingEquiv.apply_symm_apply frobeniusEquiv_symm_apply_frobenius coe_frobenius_comp_coe_frobeniusEquiv_symm Function.iterate_id

PerfectField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofCharZero 📖	mathematical	—	PerfectField	—	Irreducible.separable
ofFinite 📖	mathematical	—	PerfectField	—	CharP.exists CharP.char_is_prime IsDomain.to_noZeroDivisors instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing PerfectRing.toPerfectField expChar_prime PerfectRing.ofFiniteOfIsReduced isReduced_of_noZeroDivisors
separable_iff_squarefree 📖	mathematical	—	Polynomial.Separable Semifield.toCommSemiring Field.toSemifield Squarefree Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	Polynomial.Separable.squarefree isCoprime_of_irreducible_dvd Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain Squarefree.ne_zero Polynomial.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsCoprime.dvd_of_dvd_mul_left separable_of_irreducible dvd_add_left dvd_mul_right Polynomial.derivative_mul Irreducible.not_isUnit mul_dvd_mul_left
separable_of_irreducible 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Separable Semifield.toCommSemiring	—	—
toPerfectRing 📖	mathematical	—	PerfectRing Semifield.toCommSemiring Field.toSemifield	—	PerfectRing.ofSurjective isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain pow_one not_forall_not X_pow_sub_C_irreducible_of_prime separable_of_irreducible Polynomial.derivative_sub Polynomial.derivative_X_pow CharP.cast_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul Polynomial.derivative_C sub_self Polynomial.degree_X_pow_sub_C Nat.Prime.pos IsLocalRing.toNontrivial Field.instIsLocalRing WithBot.charZero Nat.instCharZero Nat.Prime.ne_zero

PerfectRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_frobenius 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius	—	—
ofFiniteOfIsReduced 📖	mathematical	—	PerfectRing CommRing.toCommSemiring	—	ofSurjective Finite.surjective_of_injective
ofSurjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius	PerfectRing	—	—
toPerfectField 📖	mathematical	—	PerfectField	—	Irreducible.separable Polynomial.separable_or

Polynomial

Definitions

Name	Category	Theorems
rootsExpandEquivRoots 📖	CompOp	1 math math: rootsExpandEquivRoots_apply
rootsExpandPowEquivRoots 📖	CompOp	1 math math: rootsExpandPowEquivRoots_apply
rootsExpandPowToRoots 📖	CompOp	1 math math: rootsExpandPowToRoots_apply
rootsExpandToRoots 📖	CompOp	1 math math: rootsExpandToRoots_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rootsExpandEquivRoots_apply 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset roots DFunLike.coe Equiv AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand EquivLike.toFunLike Equiv.instEquivLike rootsExpandEquivRoots Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
rootsExpandPowEquivRoots_apply 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset roots DFunLike.coe Equiv AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid EquivLike.toFunLike Equiv.instEquivLike rootsExpandPowEquivRoots MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
rootsExpandPowToRoots_apply 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset roots DFunLike.coe Function.Embedding AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid Function.instFunLikeEmbedding rootsExpandPowToRoots MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
rootsExpandToRoots_apply 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Multiset.toFinset roots DFunLike.coe Function.Embedding AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Function.instFunLikeEmbedding rootsExpandToRoots Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
roots_X_pow_char_pow_sub_C 📖	mathematical	—	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X Nat.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.instSingleton RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm iterateFrobeniusEquiv	—	roots_expand_pow expand_C expand_X map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Multiset.map_singleton roots_X_sub_C
roots_X_pow_char_pow_sub_C_pow 📖	mathematical	—	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub CommRing.toRing X Nat.instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.instSingleton RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm iterateFrobeniusEquiv	—	roots_pow roots_X_pow_char_pow_sub_C SemigroupAction.mul_smul
roots_X_pow_char_sub_C 📖	mathematical	—	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.instSingleton RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	roots_X_pow_char_pow_sub_C iterateFrobeniusEquiv_one pow_one
roots_X_pow_char_sub_C_pow 📖	mathematical	—	roots Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.instSingleton RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	roots_X_pow_char_pow_sub_C_pow iterateFrobeniusEquiv_one pow_one
roots_expand 📖	mathematical	—	roots DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	pow_one roots_expand_pow iterateFrobeniusEquiv_eq_pow
roots_expand_image_frobenius 📖	mathematical	—	Finset.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius Multiset.toFinset roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand	—	Finset.image_toFinset roots_expand_map_frobenius Multiset.toFinset_nsmul LT.lt.ne' expChar_pos
roots_expand_image_frobenius_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius Multiset.toFinset roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand	—	iterateFrobenius_one pow_one roots_expand_pow_image_iterateFrobenius_subset
roots_expand_image_iterateFrobenius 📖	mathematical	—	Finset.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike iterateFrobenius Multiset.toFinset roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid	—	Finset.image_toFinset roots_expand_pow_map_iterateFrobenius Multiset.toFinset_nsmul LT.lt.ne' expChar_pow_pos
roots_expand_map_frobenius 📖	mathematical	—	Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid	—	Multiset.map_congr roots_expand Multiset.map_nsmul Multiset.map_map frobenius_apply_frobeniusEquiv_symm Multiset.map_id'
roots_expand_map_frobenius_le 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid	—	iterateFrobenius_one Multiset.map_congr pow_one roots_expand_pow_map_iterateFrobenius_le
roots_expand_pow 📖	mathematical	—	roots DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid Multiset.map RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm iterateFrobeniusEquiv	—	Multiset.ext' count_roots rootMultiplicity_expand_pow Multiset.count_nsmul Multiset.count_map Multiset.count_eq_card_filter_eq RingEquiv.eq_symm_apply
roots_expand_pow_image_iterateFrobenius_subset 📖	mathematical	—	Finset Finset.instHasSubset Finset.image DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike iterateFrobenius Multiset.toFinset roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid	—	Finset.image_toFinset Multiset.toFinset_nsmul LT.lt.ne' expChar_pow_pos Multiset.toFinset_subset Multiset.subset_of_le roots_expand_pow_map_iterateFrobenius_le
roots_expand_pow_map_iterateFrobenius 📖	mathematical	—	Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike iterateFrobenius roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid	—	Multiset.map_congr roots_expand_pow Multiset.map_nsmul Multiset.map_map RingEquiv.apply_symm_apply Multiset.map_id'
roots_expand_pow_map_iterateFrobenius_le 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder Multiset.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike iterateFrobenius roots AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toNatPow Nat.instMonoid AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid	—	Multiset.le_iff_count Multiset.count_nsmul count_roots Multiset.count_map Multiset.count_eq_card_filter_eq Multiset.card_le_card Multiset.monotone_filter_right isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors Multiset.ext' Multiset.count_filter_of_neg Multiset.count_zero

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instFunLike RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	Equiv.injective frobenius_apply_frobeniusEquiv_symm RingEquiv.apply_symm_apply
map_iterate_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instFunLike Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	MonoidHom.map_iterate_frobeniusEquiv_symm

(root)

Definitions

Name	Category	Theorems
PerfectField 📖	CompData	11 math math: PerfectRing.toPerfectField, perfectField_of_isSeparable_of_perfectField_top, Algebra.IsAlgebraic.perfectField, perfectField_of_perfectClosure_eq_bot, PerfectField.ofFinite, perfectField_iff_splits_of_natSepDegree_eq_one, perfectField_iff_isSeparable_algebraicClosure, PerfectClosure.instPerfectField, perfectClosure.perfectField, PerfectField.ofCharZero, IsAlgClosed.perfectField
PerfectRing 📖	CompData	9 math math: Perfection.perfectRing, PreTilt.instPerfectRing, PerfectClosure.instPerfectRing, PerfectRing.ofFiniteOfIsReduced, PerfectField.toPerfectRing, PerfectRing.ofSurjective, perfectClosure.perfectRing, instPerfectRingProd, IsAlgClosed.perfectRing
frobeniusEquiv 📖	CompOp	32 math math: Polynomial.roots_expand, frobeniusEquiv_apply, coe_frobeniusEquiv_symm_comp_coe_frobenius, WittVector.frobeniusEquiv_symm_apply, iterateFrobeniusEquiv_one, frobeniusEquiv_symm_comp_frobenius, MonoidHom.map_frobeniusEquiv_symm, PreTilt.coeff_frobeniusEquiv_symm, iterateFrobeniusEquiv_eq_pow, PreTilt.coeff_iterate_frobeniusEquiv_symm, frobeniusEquiv_symm_pow, coe_frobeniusEquiv, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, frobenius_comp_frobeniusEquiv_symm, iterateFrobeniusEquiv_symm, Polynomial.roots_X_pow_char_sub_C_pow, coe_frobenius_comp_coe_frobeniusEquiv_symm, RingHom.map_iterate_frobeniusEquiv_symm, frobeniusEquiv_def, iterate_frobeniusEquiv_symm_pow_p_pow, polynomial_expand_eq, frobeniusEquiv_symm_pow_p, frobenius_apply_frobeniusEquiv_symm, Perfection.coeff_frobeniusEquiv_symm, Perfection.lift_apply_apply_coe, PreTilt.untilt_iterate_frobeniusEquiv_symm_pow, PerfectionMap.surjective, Polynomial.roots_X_pow_char_sub_C, Perfection.coeff_iterate_frobeniusEquiv_symm, MonoidHom.map_iterate_frobeniusEquiv_symm, RingHom.map_frobeniusEquiv_symm, frobeniusEquiv_symm_apply_frobenius
iterateFrobeniusEquiv 📖	CompOp	20 math math: iterateFrobeniusEquiv_symm_add, iterateFrobeniusEquiv_symm_add_apply, iterateFrobeniusEquiv_one, iterateFrobeniusEquiv_def, Polynomial.roots_X_pow_char_pow_sub_C_pow, iterateFrobeniusEquiv_add_apply, iterateFrobeniusEquiv_eq_pow, iterateFrobeniusEquiv_zero, iterateFrobeniusEquiv_symm, iterateFrobeniusEquiv_one_apply, PerfectRing.lift_apply, IsPerfectClosure.equiv_apply, iterateFrobeniusEquiv_apply, iterateFrobeniusEquiv_add, IsPerfectClosure.equiv_symm_apply, Polynomial.roots_expand_pow, PerfectRing.liftAux_apply, coe_iterateFrobeniusEquiv, iterateFrobeniusEquiv_zero_apply, Polynomial.roots_X_pow_char_pow_sub_C

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_frobenius 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius	—	PerfectRing.bijective_frobenius
bijective_iterateFrobenius 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike iterateFrobenius	—	Function.Bijective.iterate bijective_frobenius coe_iterateFrobenius
coe_frobeniusEquiv 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike frobeniusEquiv RingHom RingHom.instFunLike frobenius	—	—
coe_frobeniusEquiv_symm_comp_coe_frobenius 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv RingHom RingHom.instFunLike frobenius	—	frobeniusEquiv_symm_apply_frobenius
coe_frobenius_comp_coe_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	frobenius_apply_frobeniusEquiv_symm
coe_iterateFrobeniusEquiv 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv RingHom RingHom.instFunLike iterateFrobenius	—	—
frobeniusEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike frobeniusEquiv RingHom RingHom.instFunLike frobenius	—	—
frobeniusEquiv_def 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike frobeniusEquiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—
frobeniusEquiv_symm_apply_frobenius 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv RingHom RingHom.instFunLike frobenius	—	Function.leftInverse_surjInv PerfectRing.bijective_frobenius
frobeniusEquiv_symm_comp_frobenius 📖	mathematical	—	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm frobeniusEquiv frobenius RingHom.id	—	RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass frobeniusEquiv_symm_apply_frobenius
frobeniusEquiv_symm_pow 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingEquiv.symm_apply_apply
frobeniusEquiv_symm_pow_p 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	frobenius_apply_frobeniusEquiv_symm
frobenius_apply_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	Function.surjInv_eq Function.Bijective.surjective PerfectRing.bijective_frobenius
frobenius_comp_frobeniusEquiv_symm 📖	mathematical	—	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring frobenius RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm frobeniusEquiv RingHom.id	—	RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass frobenius_apply_frobeniusEquiv_symm
injective_frobenius 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius	—	bijective_frobenius
injective_pow_p 📖	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	—	RingEquiv.injective
instPerfectRingProd 📖	mathematical	—	PerfectRing Prod.instCommSemiring instExpCharProd AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	instExpCharProd Function.Bijective.prodMap bijective_frobenius
iterateFrobeniusEquiv_add 📖	mathematical	—	iterateFrobeniusEquiv RingEquiv.trans Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd	—	RingEquiv.ext iterateFrobeniusEquiv_add_apply
iterateFrobeniusEquiv_add_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv	—	iterateFrobenius_add_apply
iterateFrobeniusEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv RingHom RingHom.instFunLike iterateFrobenius	—	—
iterateFrobeniusEquiv_def 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	—
iterateFrobeniusEquiv_eq_pow 📖	mathematical	—	iterateFrobeniusEquiv RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup frobeniusEquiv	—	DFunLike.ext' map_pow MonoidHom.instMonoidHomClass Equiv.Perm.coe_pow pow_iterate
iterateFrobeniusEquiv_one 📖	mathematical	—	iterateFrobeniusEquiv frobeniusEquiv	—	RingEquiv.ext iterateFrobeniusEquiv_one_apply
iterateFrobeniusEquiv_one_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	iterateFrobeniusEquiv_def pow_one
iterateFrobeniusEquiv_symm 📖	mathematical	—	RingEquiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd iterateFrobeniusEquiv RingEquiv Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup frobeniusEquiv	—	iterateFrobeniusEquiv_eq_pow inv_pow
iterateFrobeniusEquiv_symm_add 📖	mathematical	—	RingEquiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd iterateFrobeniusEquiv RingEquiv.trans	—	RingEquiv.ext iterateFrobeniusEquiv_symm_add_apply
iterateFrobeniusEquiv_symm_add_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm iterateFrobeniusEquiv	—	RingEquiv.injective RingEquiv.apply_symm_apply add_comm iterateFrobeniusEquiv_add_apply
iterateFrobeniusEquiv_zero 📖	mathematical	—	iterateFrobeniusEquiv RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd	—	RingEquiv.ext iterateFrobeniusEquiv_zero_apply
iterateFrobeniusEquiv_zero_apply 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike iterateFrobeniusEquiv	—	iterateFrobeniusEquiv_def pow_zero pow_one
iterate_frobeniusEquiv_symm_pow_p_pow 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Nat.iterate DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv Nat.instMonoid	—	pow_zero pow_one pow_succ pow_mul frobeniusEquiv_symm_pow_p
not_irreducible_expand 📖	mathematical	—	Irreducible Polynomial CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring DFunLike.coe AlgHom Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.expand	—	expChar_prime RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass polynomial_expand_eq not_irreducible_pow Nat.Prime.ne_one Fact.out
polynomial_expand_eq 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.expand Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.map RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm frobeniusEquiv	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Polynomial.map_frobenius_expand Polynomial.map_expand Polynomial.map_map frobenius_comp_frobeniusEquiv_symm Polynomial.map_id
surjective_frobenius 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius	—	bijective_frobenius

---

← Back to Index