Perfection

📁 Source: Mathlib/RingTheory/Perfection.lean

Statistics

Metric	Count
Definitions ModP, preVal, perfection, Perfection, coeff, coeffMonoidHom, instCommMonoid, instCommRing, instCommSemiring, instRing, liftMonoidHom, map, mapMonoidHom, pthRoot, pthRootMonoidHom, submonoid, subring, subsemiring, PerfectionMap, equiv, map, PreTilt, coeff, instCommRing, val, valAux, Perfection, perfectionSubring, perfectionSubsemiring, Tilt, instField	31
Theorems instCharPOfPrimeOfFactNotIsUnitCast, instNontrivialOfPrimeOfFactNotIsUnitCast, mul_ne_zero_of_pow_p_ne_zero, preVal_add, preVal_eq_zero, preVal_mk, preVal_mul, preVal_zero, v_p_lt_preVal, v_p_lt_val, coe_pthRootMonoidHom_eq_powMulEquiv_symm, coe_pthRoot_eq_symm_frobeniusEquiv, coeffMonoidHom_eq_coeff, coeffMonoidHom_iterate_powMonoidHom, coeffMonoidHom_iterate_powMonoidHom', coeffMonoidHom_iterate_symm_powMulEquiv, coeffMonoidHom_mapMonoidHom, coeffMonoidHom_mk, coeffMonoidHom_powMonoidHom, coeffMonoidHom_pow_p, coeffMonoidHom_pow_p', coeffMonoidHom_pow_p_pow, coeffMonoidHom_pow_p_pow', coeffMonoidHom_pow_p_pow_self, coeffMonoidHom_pthRootMonoidHom, coeffMonoidHom_symm_powMulEquiv, coeffMonoidHom_zero_liftMonoidHom, coeff_add_ne_zero, coeff_frobenius, coeff_iterate_frobenius, coeff_iterate_frobenius', coeff_iterate_symm_frobeniusEquiv, coeff_map, coeff_mapMonoidHom, coeff_mk, coeff_ne_zero_of_le, coeff_pow_p, coeff_pow_p', coeff_surjective, coeff_symm_frobeniusEquiv, coeff_toMonoidHom, ext, extMonoid, extMonoid_iff, ext_iff, frobenius_pthRoot, hom_ext, instCharP, instPerfectRing, liftMonoidHom_symm_apply, lift_apply_apply_coe, lift_symm_apply, pthRootMonoidHom_eq_powMulEquiv_symm, pthRootMonoidHom_eq_pthRoot, pthRootMonoidHom_eq_symm_frobeniusEquiv, pthRoot_eq_symm_frobeniusEquiv, pthRoot_frobenius, comp_equiv, comp_equiv', comp_map, comp_symm_equiv, comp_symm_equiv', equiv_apply, hom_ext, id, injective, lift_apply, lift_symm_apply, map_eq_map, map_map, mk', of, surjective, coeff_def, coeff_frobenius, coeff_frobeniusEquiv_symm, coeff_iterate_frobenius, coeff_iterate_frobenius', coeff_iterate_frobeniusEquiv_symm, coeff_nat_find_add_ne_zero, coeff_pow_p, instCharP, instPerfectRing, isDomain, map_eq_zero, valAux_add, valAux_eq, valAux_mul, valAux_one, valAux_zero	90
Total	121

ModP

Definitions

Name	Category	Theorems
preVal 📖	CompOp	7 math math: PreTilt.valAux_eq, preVal_mul, preVal_mk, v_p_lt_preVal, preVal_zero, preVal_add, preVal_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCharPOfPrimeOfFactNotIsUnitCast 📖	mathematical	—	CharP ModP AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Ideal.Quotient.instRingQuotient Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast CommRing.toRing	—	CharP.quotient Fact.out
instNontrivialOfPrimeOfFactNotIsUnitCast 📖	mathematical	—	Nontrivial ModP	—	CharP.nontrivial_of_char_ne_one Nat.Prime.ne_one Fact.out instCharPOfPrimeOfFactNotIsUnitCast
mul_ne_zero_of_pow_p_ne_zero 📖	—	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	—	—	Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Nat.Prime.pos Fact.out RingHom.map_mul v_p_lt_val map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Valuation.map_mul lt_of_le_of_lt zero_le zero_lt_iff NNReal.rpow_one NNReal.rpow_add ne_of_gt NNReal.rpow_le_rpow_of_exponent_ge Valuation.Integers.map_le_one map_natCast add_div div_le_one Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Nat.Prime.two_le mul_lt_mul'' LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOrderedRing.toMulPosMono mul_one_div_cancel Nat.cast_ne_zero Nat.Prime.ne_zero NNReal.rpow_mul NNReal.rpow_natCast NNReal.rpow_lt_rpow_iff Valuation.map_pow map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.map_pow zero_le'
preVal_add 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder preVal ModP Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SemilatticeSup.toMax NNReal.instSemilatticeSup	—	zero_add le_max_right add_zero le_max_left preVal_zero zero_le Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Valuation.map_add
preVal_eq_zero 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	preVal NNReal NNReal.instZero ModP Submodule.Quotient.instZeroQuotient CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	by_contradiction not_lt_zero' v_p_lt_preVal preVal_zero
preVal_mk 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	preVal DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Valuation NNReal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield algebraMap	—	Ideal.instIsTwoSided_1 Ideal.mem_span_singleton' Ideal.Quotient.eq Quotient.sound' Quotient.mk_out' Valuation.map_eq_of_sub_lt lt_of_not_ge map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Valuation.Integers.le_iff_dvd Ideal.Quotient.eq_zero_iff_mem Ideal.mem_span_singleton dvd_of_mul_left_dvd
preVal_mul 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	preVal ModP Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NNReal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	MulZeroClass.zero_mul MulZeroClass.mul_zero Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Valuation.map_mul
preVal_zero 📖	mathematical	—	preVal ModP Submodule.Quotient.instZeroQuotient CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NNReal NNReal.instZero	—	—
v_p_lt_preVal 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne preVal	—	not_lt_zero' preVal_zero lt_of_not_ge Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective Ideal.Quotient.eq_zero_iff_mem Ideal.mem_span_singleton Valuation.Integers.le_iff_dvd map_natCast RingHom.instRingHomClass
v_p_lt_val 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap	—	Ideal.instIsTwoSided_1 lt_iff_not_ge not_iff_not map_natCast RingHom.instRingHomClass Valuation.Integers.le_iff_dvd Ideal.Quotient.eq_zero_iff_mem Ideal.mem_span_singleton

Monoid

Definitions

Name	Category	Theorems
perfection 📖	CompOp	—

Perfection

Definitions

Name	Category	Theorems
coeff 📖	CompOp	28 math math: mk_comp_teichmuller₀, PerfectionMap.map_eq_map, coeff_iterate_symm_frobeniusEquiv, coeff_toMonoidHom, mk_teichmuller, coeff_symm_frobeniusEquiv, coeff_map, coeff_mapMonoidHom, mk_comp_teichmuller', coeff_mk, coeff_quotientMulEquiv, coeff_iterate_frobenius, coeffMonoidHom_eq_coeff, PerfectionMap.comp_equiv', ext_iff, mk_comp_teichmuller, PerfectionMap.comp_equiv, PerfectionMap.comp_symm_equiv, coeff_surjective, mk_teichmuller₀, PerfectionMap.comp_symm_equiv', lift_symm_apply, PerfectionMap.of, coeff_pow_p, coeff_iterate_frobenius', coeff_pow_p', PreTilt.coeff_def, coeff_frobenius
coeffMonoidHom 📖	CompOp	22 math math: coeffMonoidHom_powMonoidHom, coeff_toMonoidHom, coeff_mapMonoidHom, coeff_quotientMulEquiv, coeffMonoidHom_mk, coeffMonoidHom_eq_coeff, coeffMonoidHom_pow_p', coeffMonoidHom_pow_p_pow', liftMonoidHom_symm_apply, coeffMonoidHom_iterate_powMonoidHom', coeffMonoidHom_pthRootMonoidHom, coeffMonoidHom_zero_liftMonoidHom, coeffMonoidHom_symm_powMulEquiv, coeffMonoidHom_pow_p_pow_self, coeffMonoidHom_pow_p, coeff_zero_symm_quotientMulEquiv, coeffMonoidHom_mapMonoidHom, coeffMonoidHom_pow_p_pow, coeffMonoidHom_iterate_symm_powMulEquiv, teichmuller₀_mapMonoidHom_idealQuotientMk, extMonoid_iff, coeffMonoidHom_iterate_powMonoidHom
instCommMonoid 📖	CompOp	26 math math: pthRootMonoidHom_eq_powMulEquiv_symm, coeffMonoidHom_powMonoidHom, coeff_mapMonoidHom, coeff_quotientMulEquiv, coeffMonoidHom_mk, coeffMonoidHom_eq_coeff, coeffMonoidHom_pow_p', coeffMonoidHom_pow_p_pow', liftMonoidHom_symm_apply, coeffMonoidHom_iterate_powMonoidHom', pthRootMonoidHom_eq_pthRoot, instPerfectRing, coeffMonoidHom_pthRootMonoidHom, pthRootMonoidHom_eq_symm_frobeniusEquiv, coeffMonoidHom_zero_liftMonoidHom, coeffMonoidHom_symm_powMulEquiv, coeffMonoidHom_pow_p_pow_self, coeffMonoidHom_pow_p, coeff_zero_symm_quotientMulEquiv, coeffMonoidHom_mapMonoidHom, coe_pthRootMonoidHom_eq_powMulEquiv_symm, coeffMonoidHom_pow_p_pow, coeffMonoidHom_iterate_symm_powMulEquiv, teichmuller₀_mapMonoidHom_idealQuotientMk, extMonoid_iff, coeffMonoidHom_iterate_powMonoidHom
instCommRing 📖	CompOp	3 math math: coeff_quotientMulEquiv, teichmuller_zero, coeff_zero_symm_quotientMulEquiv
instCommSemiring 📖	CompOp	50 math math: pthRoot_frobenius, mk_comp_teichmuller₀, PerfectionMap.map_eq_map, coeff_iterate_symm_frobeniusEquiv, coeff_toMonoidHom, coe_pthRoot_eq_symm_frobeniusEquiv, mk_teichmuller, teichmuller₀_spec, coeff_symm_frobeniusEquiv, coeff_map, coeff_mapMonoidHom, instCharP, mk_comp_teichmuller', coeff_mk, coeff_quotientMulEquiv, coeff_iterate_frobenius, coeffMonoidHom_eq_coeff, teichmuller_sModEq, PerfectionMap.comp_equiv', teichmuller₀_sModEq, teichmuller₀_spec', ext_iff, mk_comp_teichmuller, PerfectionMap.comp_equiv, teichmuller_zero, PerfectionMap.comp_symm_equiv, coeff_surjective, pthRootMonoidHom_eq_pthRoot, coe_teichmuller_eq_teichmuller₀, pthRootMonoidHom_eq_symm_frobeniusEquiv, teichmuller_eq_teichmuller₀_toMonoidHom, lift_apply_apply_coe, pthRoot_eq_symm_frobeniusEquiv, mk_teichmuller₀, coeff_zero_symm_quotientMulEquiv, PerfectionMap.comp_symm_equiv', lift_symm_apply, PerfectionMap.of, coeff_pow_p, coeff_iterate_frobenius', teichmuller₀_mapMonoidHom_idealQuotientMk, PerfectionMap.lift_apply, coeff_pow_p', PreTilt.coeff_def, PerfectionMap.equiv_apply, teichmuller_spec, frobenius_pthRoot, teichmuller_spec', coeff_frobenius, teichmullerFun_eq_teichmuller₀
instRing 📖	CompOp	—
liftMonoidHom 📖	CompOp	2 math math: liftMonoidHom_symm_apply, coeffMonoidHom_zero_liftMonoidHom
map 📖	CompOp	2 math math: PerfectionMap.map_eq_map, coeff_map
mapMonoidHom 📖	CompOp	3 math math: coeff_mapMonoidHom, coeffMonoidHom_mapMonoidHom, teichmuller₀_mapMonoidHom_idealQuotientMk
pthRoot 📖	CompOp	5 math math: pthRoot_frobenius, coe_pthRoot_eq_symm_frobeniusEquiv, pthRootMonoidHom_eq_pthRoot, pthRoot_eq_symm_frobeniusEquiv, frobenius_pthRoot
pthRootMonoidHom 📖	CompOp	5 math math: pthRootMonoidHom_eq_powMulEquiv_symm, pthRootMonoidHom_eq_pthRoot, coeffMonoidHom_pthRootMonoidHom, pthRootMonoidHom_eq_symm_frobeniusEquiv, coe_pthRootMonoidHom_eq_powMulEquiv_symm
submonoid 📖	CompOp	—
subring 📖	CompOp	—
subsemiring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pthRootMonoidHom_eq_powMulEquiv_symm 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike pthRootMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm powMulEquiv instPerfectRing	—	instPerfectRing MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass pthRootMonoidHom_eq_powMulEquiv_symm
coe_pthRoot_eq_symm_frobeniusEquiv 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike pthRoot RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing CommSemiring.toCommMonoid	—	expChar_prime instCharP instPerfectRing RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass pthRoot_eq_symm_frobeniusEquiv
coeffMonoidHom_eq_coeff 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid CommSemiring.toCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom RingHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	—
coeffMonoidHom_iterate_powMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.iterate powMonoidHom	—	Function.iterate_succ_apply' coeffMonoidHom_powMonoidHom
coeffMonoidHom_iterate_powMonoidHom' 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.iterate powMonoidHom	—	coeffMonoidHom_iterate_powMonoidHom
coeffMonoidHom_iterate_symm_powMulEquiv 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.iterate MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm powMulEquiv instPerfectRing	—	instPerfectRing Function.iterate_succ_apply' coeffMonoidHom_symm_powMulEquiv
coeffMonoidHom_mapMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom mapMonoidHom	—	—
coeffMonoidHom_mk 📖	mathematical	Monoid.toPow CommMonoid.toMonoid	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom	—	—
coeffMonoidHom_powMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom powMonoidHom	—	coeffMonoidHom_pow_p
coeffMonoidHom_pow_p 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom	—	map_pow MonoidHom.instMonoidHomClass
coeffMonoidHom_pow_p' 📖	mathematical	—	Monoid.toPow CommMonoid.toMonoid DFunLike.coe MonoidHom Perfection MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom	—	—
coeffMonoidHom_pow_p_pow 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.instMonoid	—	add_zero pow_zero pow_one pow_succ pow_mul coeffMonoidHom_pow_p
coeffMonoidHom_pow_p_pow' 📖	mathematical	—	Monoid.toPow CommMonoid.toMonoid DFunLike.coe MonoidHom Perfection MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.instMonoid	—	map_pow MonoidHom.instMonoidHomClass coeffMonoidHom_pow_p_pow
coeffMonoidHom_pow_p_pow_self 📖	mathematical	—	Monoid.toPow CommMonoid.toMonoid DFunLike.coe MonoidHom Perfection MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom Nat.instMonoid	—	coeffMonoidHom_pow_p_pow' zero_add
coeffMonoidHom_pthRootMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom pthRootMonoidHom	—	—
coeffMonoidHom_symm_powMulEquiv 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm powMulEquiv instPerfectRing	—	instPerfectRing coe_pthRootMonoidHom_eq_powMulEquiv_symm
coeffMonoidHom_zero_liftMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom MulEquiv MonoidHom.mul EquivLike.toFunLike MulEquiv.instEquivLike liftMonoidHom	—	pow pow_zero powMulEquiv.congr_simp powMulEquiv_one
coeff_add_ne_zero 📖	—	—	—	—	coeff_pow_p map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_pow Nat.Prime.ne_zero Fact.out
coeff_frobenius 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	coeffMonoidHom_powMonoidHom
coeff_iterate_frobenius 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff Nat.iterate frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	coeffMonoidHom_iterate_powMonoidHom
coeff_iterate_frobenius' 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff Nat.iterate frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	coeffMonoidHom_iterate_powMonoidHom'
coeff_iterate_symm_frobeniusEquiv 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing CommSemiring.toCommMonoid	—	coeffMonoidHom_iterate_symm_powMulEquiv
coeff_map 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff map	—	—
coeff_mapMonoidHom 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff MonoidHom CommMonoid.toMonoid CommRing.toCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike mapMonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass coeffMonoidHom	—	—
coeff_mk 📖	mathematical	Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	—
coeff_ne_zero_of_le 📖	—	—	—	—	coeff_add_ne_zero
coeff_pow_p 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	coeffMonoidHom_pow_p
coeff_pow_p' 📖	mathematical	—	Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Perfection Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	—
coeff_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	expChar_prime Nat.leRec_succ instReflLe Nat.leRec_self IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd add_tsub_cancel_left Nat.instOrderedSub eq_natCast RingHom.instRingHomClass expChar_one Nat.instCharZero pow_succ pow_mul
coeff_symm_frobeniusEquiv 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing CommSemiring.toCommMonoid	—	coeffMonoidHom_symm_powMulEquiv
coeff_toMonoidHom 📖	mathematical	—	RingHom.toMonoidHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring coeff coeffMonoidHom CommSemiring.toCommMonoid	—	—
ext 📖	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	—	extMonoid
extMonoid 📖	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom	—	—	—
extMonoid_iff 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom	—	extMonoid
ext_iff 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	ext
frobenius_pthRoot 📖	mathematical	—	RingHom.comp Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP pthRoot RingHom.id	—	pthRoot_frobenius
hom_ext 📖	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff	—	—	Equiv.injective RingHom.ext
instCharP 📖	mathematical	—	CharP Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiring	—	CharP.subsemiring CharP.pi
instPerfectRing 📖	mathematical	—	PerfectRing Perfection Monoid.toPow CommMonoid.toMonoid instCommMonoid	—	Function.bijective_iff_has_inverse extMonoid map_pow MonoidHom.instMonoidHomClass coeffMonoidHom_pow_p'
liftMonoidHom_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm liftMonoidHom MonoidHom.comp coeffMonoidHom	—	—
lift_apply_apply_coe 📖	mathematical	—	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike lift Nat.iterate RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv	—	—
lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift RingHom.comp coeff	—	—
pthRootMonoidHom_eq_powMulEquiv_symm 📖	mathematical	—	pthRootMonoidHom MonoidHomClass.toMonoidHom Perfection Monoid.toPow CommMonoid.toMonoid MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulEquiv.symm powMulEquiv instPerfectRing	—	MonoidHom.ext MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass instPerfectRing MulEquiv.eq_symm_apply extMonoid map_pow MonoidHom.instMonoidHomClass coeffMonoidHom_pow_p'
pthRootMonoidHom_eq_pthRoot 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid CommSemiring.toCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike pthRootMonoidHom RingHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike pthRoot	—	—
pthRootMonoidHom_eq_symm_frobeniusEquiv 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid CommSemiring.toCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike pthRootMonoidHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring RingHom.instFunLike RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass expChar_prime instCharP instPerfectRing RingEquivClass.toMulEquivClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass pthRootMonoidHom_eq_powMulEquiv_symm
pthRoot_eq_symm_frobeniusEquiv 📖	mathematical	—	pthRoot RingHomClass.toRingHom RingEquiv Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instCommSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing CommSemiring.toCommMonoid	—	RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass expChar_prime instCharP instPerfectRing ext coeffMonoidHom_pow_p'
pthRoot_frobenius 📖	mathematical	—	RingHom.comp Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring instCommSemiring pthRoot frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP RingHom.id	—	RingHom.ext expChar_prime instCharP ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass instPerfectRing pthRoot_eq_symm_frobeniusEquiv frobeniusEquiv_symm_comp_frobenius

PerfectionMap

Definitions

Name	Category	Theorems
equiv 📖	CompOp	6 math math: comp_equiv', comp_equiv, comp_symm_equiv, comp_symm_equiv', lift_apply, equiv_apply
map 📖	CompOp	3 math math: map_eq_map, map_map, comp_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_equiv 📖	mathematical	PerfectionMap	DFunLike.coe RingHom Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring Perfection.instCommSemiring RingHom.instFunLike Perfection.coeff RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv	—	—
comp_equiv' 📖	mathematical	PerfectionMap	RingHom.comp Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring Perfection.instCommSemiring Perfection.coeff RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass equiv	—	RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
comp_map 📖	mathematical	PerfectionMap	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring map	—	Equiv.symm_apply_apply
comp_symm_equiv 📖	mathematical	PerfectionMap	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingEquiv Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Perfection.instCommSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equiv Perfection.coeff	—	comp_equiv RingEquiv.apply_symm_apply
comp_symm_equiv' 📖	mathematical	PerfectionMap	RingHom.comp Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Semiring.toNonAssocSemiring Perfection.instCommSemiring RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.symm equiv Perfection.coeff	—	RingHom.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass comp_symm_equiv
equiv_apply 📖	mathematical	PerfectionMap	DFunLike.coe RingEquiv Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Perfection.instCommSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike equiv RingHom RingHom.instFunLike Equiv Equiv.instEquivLike Perfection.lift	—	—
hom_ext 📖	—	PerfectionMap DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	—	Equiv.injective RingHom.ext
id 📖	mathematical	—	PerfectionMap RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	expChar_prime injective_pow_p Function.iterate_succ_apply' frobeniusEquiv_symm_pow_p
injective 📖	—	PerfectionMap DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—	—
lift_apply 📖	mathematical	PerfectionMap	DFunLike.coe Equiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike lift RingHom.comp Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Perfection.instCommSemiring RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingEquiv.instEquivLike RingEquiv.symm equiv Perfection.lift	—	—
lift_symm_apply 📖	mathematical	PerfectionMap	DFunLike.coe Equiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift RingHom.comp	—	—
map_eq_map 📖	mathematical	—	map Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Perfection.instCommSemiring Perfection.instCharP Perfection.instPerfectRing CommSemiring.toCommMonoid Perfection.coeff of Perfection.map	—	hom_ext Perfection.instCharP Perfection.instPerfectRing of map_map Perfection.coeff_map
map_map 📖	mathematical	PerfectionMap	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike map	—	RingHom.ext_iff comp_map
mk' 📖	mathematical	DFunLike.coe Equiv RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Perfection.instCommSemiring EquivLike.toFunLike Equiv.instEquivLike Perfection.lift RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingEquiv.instEquivLike RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	PerfectionMap	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass expChar_prime RingEquiv.injective RingHom.ext_iff Perfection.ext RingEquiv.surjective
of 📖	mathematical	—	PerfectionMap Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Perfection.instCommSemiring Perfection.instCharP Perfection.instPerfectRing CommSemiring.toCommMonoid Perfection.coeff	—	mk' Perfection.instCharP Perfection.instPerfectRing RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass Equiv.apply_eq_iff_eq_symm_apply
surjective 📖	mathematical	PerfectionMap Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—

PreTilt

Definitions

Name	Category	Theorems
coeff 📖	CompOp	12 math math: valAux_eq, coeff_pow_p, mk_comp_untilt_eq_coeff_zero, coeff_frobeniusEquiv_symm, coeff_frobenius, coeff_iterate_frobeniusEquiv_symm, WittVector.ghostComponentModPPow_teichmuller_coeff, coeff_iterate_frobenius, mk_untilt_eq_coeff_zero, WittVector.mk_fontaineTheta, coeff_def, coeff_iterate_frobenius'
instCommRing 📖	CompOp	27 math math: valAux_eq, WittVector.factorPowSucc_comp_fontaineThetaModPPow, coeff_pow_p, instPerfectRing, WittVector.factorPowSucc_fontaineThetaModPPow_eq, mk_comp_untilt_eq_coeff_zero, WittVector.mk_pow_fontaineTheta, coeff_frobeniusEquiv_symm, valAux_zero, coeff_frobenius, coeff_iterate_frobeniusEquiv_symm, valAux_mul, WittVector.fontaineThetaModPPow_teichmuller, isDomain, WittVector.ghostComponentModPPow_teichmuller_coeff, surjective_fontaineTheta, WittVector.fontaineTheta_teichmuller, valAux_add, coeff_iterate_frobenius, valAux_one, untilt_iterate_frobeniusEquiv_symm_pow, instCharP, map_eq_zero, mk_untilt_eq_coeff_zero, WittVector.mk_fontaineTheta, coeff_def, coeff_iterate_frobenius'
val 📖	CompOp	1 math math: map_eq_zero
valAux 📖	CompOp	5 math math: valAux_eq, valAux_zero, valAux_mul, valAux_add, valAux_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_def 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff Perfection Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring Perfection.instCommSemiring ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff	—	—
coeff_frobenius 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	expChar_prime instCharP ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_frobenius
coeff_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing	—	expChar_prime instCharP instPerfectRing ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_symm_frobeniusEquiv
coeff_iterate_frobenius 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff Nat.iterate frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	expChar_prime instCharP ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_iterate_frobenius
coeff_iterate_frobenius' 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff Nat.iterate frobenius expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP	—	Perfection.coeff_iterate_frobenius' ModP.instCharPOfPrimeOfFactNotIsUnitCast
coeff_iterate_frobeniusEquiv_symm 📖	mathematical	—	DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff Nat.iterate RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm frobeniusEquiv expChar_prime AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCharP instPerfectRing	—	expChar_prime instCharP instPerfectRing ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_iterate_symm_frobeniusEquiv
coeff_nat_find_add_ne_zero 📖	—	—	—	—	Perfection.coeff_add_ne_zero ModP.instCharPOfPrimeOfFactNotIsUnitCast Nat.find_spec
coeff_pow_p 📖	mathematical	—	ModP Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring Ideal.span CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom PreTilt Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike coeff	—	Perfection.coeff_pow_p ModP.instCharPOfPrimeOfFactNotIsUnitCast
instCharP 📖	mathematical	—	CharP PreTilt AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing	—	—
instPerfectRing 📖	mathematical	—	PerfectRing PreTilt Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	—
isDomain 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	IsDomain PreTilt CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	Fact.out NoZeroDivisors.to_isDomain Nontrivial.exists_pair_ne CharP.nontrivial_of_char_ne_one Nat.Prime.ne_one instCharP map_eq_zero Mathlib.Tactic.Contrapose.contrapose₁ Valuation.map_mul mul_ne_zero
map_eq_zero 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	DFunLike.coe Valuation PreTilt NNReal LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero NNReal.instLinearOrderedCommGroupWithZero CommRing.toRing instCommRing Valuation.instFunLike val NNReal.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Valuation.map_zero Perfection.ext ModP.instCharPOfPrimeOfFactNotIsUnitCast eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors valAux_eq ModP.preVal_eq_zero
valAux_add 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder valAux PreTilt Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing SemilatticeSup.toMax NNReal.instSemilatticeSup	—	zero_add valAux_zero max_eq_right zero_le le_refl add_zero max_eq_left Perfection.ext ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_ne_zero_of_le le_trans le_max_left le_max_right valAux_eq map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass le_max_iff ModP.preVal_add le_max_of_le_left pow_le_pow_left' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul le_max_of_le_right
valAux_eq 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	valAux NNReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring ModP.preVal DFunLike.coe RingHom PreTilt ModP Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.Quotient.semiring Ideal.span Set Set.instSingletonSet AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.instFunLike coeff Nat.instMonoid	—	valAux.eq_1 Nat.find_min' Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coeff_pow_p coeff_nat_find_add_ne_zero add_assoc Valuation.map_pow pow_mul pow_succ'
valAux_mul 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	valAux PreTilt Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NNReal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	MulZeroClass.zero_mul valAux_zero MulZeroClass.mul_zero Perfection.ext ModP.instCharPOfPrimeOfFactNotIsUnitCast Perfection.coeff_ne_zero_of_le le_max_left le_max_right map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass ModP.mul_ne_zero_of_pow_p_ne_zero coeff_pow_p valAux_eq Perfection.coeff_add_ne_zero ModP.preVal_mul mul_pow
valAux_one 📖	mathematical	Valuation.Integers NNReal EuclideanDomain.toCommRing Field.toEuclideanDomain NNReal.instLinearOrderedCommGroupWithZero	valAux PreTilt AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instCommRing NNReal NNReal.instOne	—	valAux_eq one_ne_zero NeZero.one ModP.instNontrivialOfPrimeOfFactNotIsUnitCast pow_zero pow_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.instIsTwoSided_1 RingHom.map_one Valuation.map_one
valAux_zero 📖	mathematical	—	valAux PreTilt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NNReal NNReal.instZero	—	—

Ring

Definitions

Name	Category	Theorems
Perfection 📖	CompOp	—
perfectionSubring 📖	CompOp	—
perfectionSubsemiring 📖	CompOp	—

Tilt

Definitions

Name	Category	Theorems
instField 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ModP 📖	CompOp	18 math math: PreTilt.valAux_eq, PreTilt.coeff_pow_p, PreTilt.mk_comp_untilt_eq_coeff_zero, PreTilt.coeff_frobeniusEquiv_symm, ModP.preVal_mul, PreTilt.coeff_frobenius, PreTilt.coeff_iterate_frobeniusEquiv_symm, ModP.instNontrivialOfPrimeOfFactNotIsUnitCast, WittVector.ghostComponentModPPow_teichmuller_coeff, ModP.preVal_zero, ModP.instCharPOfPrimeOfFactNotIsUnitCast, PreTilt.coeff_iterate_frobenius, ModP.preVal_add, ModP.preVal_eq_zero, PreTilt.mk_untilt_eq_coeff_zero, WittVector.mk_fontaineTheta, PreTilt.coeff_def, PreTilt.coeff_iterate_frobenius'
Perfection 📖	CompOp	69 math math: Perfection.pthRootMonoidHom_eq_powMulEquiv_symm, Perfection.pthRoot_frobenius, Perfection.mk_comp_teichmuller₀, Perfection.coeffMonoidHom_powMonoidHom, PerfectionMap.map_eq_map, Perfection.coeff_iterate_symm_frobeniusEquiv, Perfection.coeff_toMonoidHom, Perfection.coe_pthRoot_eq_symm_frobeniusEquiv, Perfection.mk_teichmuller, Perfection.teichmuller₀_spec, Perfection.coeff_symm_frobeniusEquiv, Perfection.coeff_map, Perfection.coeff_mapMonoidHom, Perfection.instCharP, Perfection.mk_comp_teichmuller', Perfection.coeff_mk, Perfection.coeff_quotientMulEquiv, Perfection.coeffMonoidHom_mk, Perfection.coeff_iterate_frobenius, Perfection.coeffMonoidHom_eq_coeff, Perfection.teichmuller_sModEq, PerfectionMap.comp_equiv', Perfection.teichmuller₀_sModEq, Perfection.teichmuller₀_spec', Perfection.coeffMonoidHom_pow_p', Perfection.coeffMonoidHom_pow_p_pow', Perfection.ext_iff, Perfection.mk_comp_teichmuller, PerfectionMap.comp_equiv, Perfection.teichmuller_zero, Perfection.liftMonoidHom_symm_apply, PerfectionMap.comp_symm_equiv, Perfection.coeff_surjective, Perfection.coeffMonoidHom_iterate_powMonoidHom', Perfection.pthRootMonoidHom_eq_pthRoot, Perfection.instPerfectRing, Perfection.coe_teichmuller_eq_teichmuller₀, Perfection.coeffMonoidHom_pthRootMonoidHom, Perfection.pthRootMonoidHom_eq_symm_frobeniusEquiv, Perfection.coeffMonoidHom_zero_liftMonoidHom, Perfection.coeffMonoidHom_symm_powMulEquiv, Perfection.teichmuller_eq_teichmuller₀_toMonoidHom, Perfection.lift_apply_apply_coe, Perfection.pthRoot_eq_symm_frobeniusEquiv, Perfection.mk_teichmuller₀, Perfection.coeffMonoidHom_pow_p_pow_self, Perfection.coeffMonoidHom_pow_p, Perfection.coeff_zero_symm_quotientMulEquiv, Perfection.coeffMonoidHom_mapMonoidHom, PerfectionMap.comp_symm_equiv', Perfection.lift_symm_apply, Perfection.coe_pthRootMonoidHom_eq_powMulEquiv_symm, Perfection.coeffMonoidHom_pow_p_pow, Perfection.coeffMonoidHom_iterate_symm_powMulEquiv, PerfectionMap.of, Perfection.coeff_pow_p, Perfection.coeff_iterate_frobenius', Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk, PerfectionMap.lift_apply, Perfection.coeff_pow_p', Perfection.extMonoid_iff, PreTilt.coeff_def, PerfectionMap.equiv_apply, Perfection.teichmuller_spec, Perfection.coeffMonoidHom_iterate_powMonoidHom, Perfection.frobenius_pthRoot, Perfection.teichmuller_spec', Perfection.coeff_frobenius, Perfection.teichmullerFun_eq_teichmuller₀
PerfectionMap 📖	CompData	3 math math: PerfectionMap.id, PerfectionMap.mk', PerfectionMap.of
PreTilt 📖	CompOp	27 math math: PreTilt.valAux_eq, WittVector.factorPowSucc_comp_fontaineThetaModPPow, PreTilt.coeff_pow_p, PreTilt.instPerfectRing, WittVector.factorPowSucc_fontaineThetaModPPow_eq, PreTilt.mk_comp_untilt_eq_coeff_zero, WittVector.mk_pow_fontaineTheta, PreTilt.coeff_frobeniusEquiv_symm, PreTilt.valAux_zero, PreTilt.coeff_frobenius, PreTilt.coeff_iterate_frobeniusEquiv_symm, PreTilt.valAux_mul, WittVector.fontaineThetaModPPow_teichmuller, PreTilt.isDomain, WittVector.ghostComponentModPPow_teichmuller_coeff, surjective_fontaineTheta, WittVector.fontaineTheta_teichmuller, PreTilt.valAux_add, PreTilt.coeff_iterate_frobenius, PreTilt.valAux_one, PreTilt.untilt_iterate_frobeniusEquiv_symm_pow, PreTilt.instCharP, PreTilt.map_eq_zero, PreTilt.mk_untilt_eq_coeff_zero, WittVector.mk_fontaineTheta, PreTilt.coeff_def, PreTilt.coeff_iterate_frobenius'
Tilt 📖	CompOp	—

---

← Back to Index