Perfection

📁 Source: Mathlib/RingTheory/Perfection.lean

Statistics

Metric	Count
Definitions `ModP`, `commRing`, `preVal`, `perfection`, `coeff`, `commRing`, `commSemiring`, `instInhabitedPerfection`, `map`, `pthRoot`, `PerfectionMap`, `equiv`, `map`, `PreTilt`, `coeff`, `instCommRing`, `val`, `valAux`, `Perfection`, `perfectionSubring`, `perfectionSubsemiring`, `Tilt`, `instField`	23
Theorems `charP`, `mul_ne_zero_of_pow_p_ne_zero`, `nontrivial`, `preVal_add`, `preVal_eq_zero`, `preVal_mk`, `preVal_mul`, `preVal_zero`, `v_p_lt_preVal`, `v_p_lt_val`, `charP`, `coeff_add_ne_zero`, `coeff_frobenius`, `coeff_frobeniusEquiv_symm`, `coeff_iterate_frobenius`, `coeff_iterate_frobenius'`, `coeff_iterate_frobeniusEquiv_symm`, `coeff_map`, `coeff_mk`, `coeff_ne_zero_of_le`, `coeff_pow_p`, `coeff_pow_p'`, `coeff_pthRoot`, `coeff_surjective`, `ext`, `ext_iff`, `frobenius_pthRoot`, `hom_ext`, `lift_apply_apply_coe`, `lift_symm_apply`, `map_apply_coe`, `perfectRing`, `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`	66
Total	89

ModP

Definitions

Name	Category	Theorems
`commRing` 📖	CompOp	6 math math: `preVal_mul`, `WittVector.ker_map_le_ker_mk_comp_ghostComponent`, `WittVector.ghostComponentModPPow_teichmuller_coeff`, `WittVector.quotEquivOfEq_ghostComponentModPPow`, `preVal_add`, `WittVector.ghostComponentModPPow_map_mk`
`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
`charP` 📖	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`
`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` `NNReal.instCanonicallyOrderedAdd` `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` `NNReal.instIsOrderedRing` `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'`
`nontrivial` 📖	mathematical	—	`Nontrivial` `ModP`	—	`CharP.nontrivial_of_char_ne_one` `Nat.Prime.ne_one` `Fact.out` `charP`
`preVal_add` 📖	mathematical	`Valuation.Integers` `NNReal` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NNReal.instLinearOrderedCommGroupWithZero`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `preVal` `ModP` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `NNReal.instMax`	—	`zero_add` `le_max_right` `add_zero` `le_max_left` `preVal_zero` `zero_le` `NNReal.instCanonicallyOrderedAdd` `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` `instZeroNNReal` `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` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `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` `commRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`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` `instZeroNNReal`	—	—
`v_p_lt_preVal` 📖	mathematical	`Valuation.Integers` `NNReal` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NNReal.instLinearOrderedCommGroupWithZero`	`Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `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`	`Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `Valuation` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `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	21 math math: `PerfectionMap.map_eq_map`, `coeff_map`, `coeff_mk`, `coeff_iterate_frobenius`, `map_apply_coe`, `PerfectionMap.comp_equiv'`, `ext_iff`, `PerfectionMap.comp_equiv`, `PerfectionMap.comp_symm_equiv`, `coeff_surjective`, `coeff_pthRoot`, `coeff_frobeniusEquiv_symm`, `PerfectionMap.comp_symm_equiv'`, `coeff_iterate_frobeniusEquiv_symm`, `lift_symm_apply`, `PerfectionMap.of`, `coeff_pow_p`, `coeff_iterate_frobenius'`, `coeff_pow_p'`, `PreTilt.coeff_def`, `coeff_frobenius`
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	28 math math: `pthRoot_frobenius`, `perfectRing`, `PerfectionMap.map_eq_map`, `coeff_map`, `charP`, `coeff_mk`, `coeff_iterate_frobenius`, `map_apply_coe`, `PerfectionMap.comp_equiv'`, `ext_iff`, `PerfectionMap.comp_equiv`, `PerfectionMap.comp_symm_equiv`, `coeff_surjective`, `coeff_pthRoot`, `coeff_frobeniusEquiv_symm`, `lift_apply_apply_coe`, `PerfectionMap.comp_symm_equiv'`, `coeff_iterate_frobeniusEquiv_symm`, `lift_symm_apply`, `PerfectionMap.of`, `coeff_pow_p`, `coeff_iterate_frobenius'`, `PerfectionMap.lift_apply`, `coeff_pow_p'`, `PreTilt.coeff_def`, `PerfectionMap.equiv_apply`, `frobenius_pthRoot`, `coeff_frobenius`
`instInhabitedPerfection` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `PerfectionMap.map_eq_map`, `coeff_map`, `map_apply_coe`
`pthRoot` 📖	CompOp	3 math math: `pthRoot_frobenius`, `coeff_pthRoot`, `frobenius_pthRoot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charP` 📖	mathematical	—	`CharP` `Ring.Perfection` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`CharP.subsemiring` `CharP.pi`
`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` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `charP`	—	`coeff_pow_p`
`coeff_frobeniusEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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` `charP` `perfectRing`	—	`expChar_prime` `charP` `perfectRing` `frobenius_apply_frobeniusEquiv_symm` `coeff_frobenius`
`coeff_iterate_frobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `Nat.iterate` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `charP`	—	`expChar_prime` `charP` `Function.iterate_succ_apply'` `coeff_frobenius`
`coeff_iterate_frobenius'` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `Nat.iterate` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `charP`	—	`expChar_prime` `charP` `coeff_iterate_frobenius` `tsub_add_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub`
`coeff_iterate_frobeniusEquiv_symm` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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` `charP` `perfectRing`	—	`expChar_prime` `charP` `perfectRing` `add_zero` `coeff_frobeniusEquiv_symm`
`coeff_map` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `map`	—	—
`coeff_mk` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `coeff`	—	—
`coeff_ne_zero_of_le` 📖	—	—	—	—	`coeff_add_ne_zero`
`coeff_pow_p` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coeff_pow_p'` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `coeff`	—	—
`coeff_pthRoot` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff` `pthRoot`	—	—
`coeff_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Ring.Perfection` `commSemiring` `coeff`	—	`expChar_prime` `Nat.leRec_succ` `Nat.leRec_self` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `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`
`ext` 📖	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff`	—	—	—
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff`	—	`ext`
`frobenius_pthRoot` 📖	mathematical	—	`RingHom.comp` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `charP` `pthRoot` `RingHom.id`	—	`RingHom.ext` `expChar_prime` `charP` `ext` `RingHom.comp_apply` `RingHom.id_apply` `RingHom.map_frobenius` `coeff_pthRoot` `coeff_frobenius`
`hom_ext` 📖	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `coeff`	—	—	`expChar_prime` `Equiv.injective` `RingHom.ext`
`lift_apply_apply_coe` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `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`	—	`expChar_prime`
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `RingHom.comp` `coeff`	—	`expChar_prime`
`map_apply_coe` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `map` `coeff`	—	—
`perfectRing` 📖	mathematical	—	`PerfectRing` `Ring.Perfection` `commSemiring` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `charP`	—	`expChar_prime` `charP` `Function.bijective_iff_has_inverse` `DFunLike.congr_fun` `frobenius_pthRoot` `pthRoot_frobenius`
`pthRoot_frobenius` 📖	mathematical	—	`RingHom.comp` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `pthRoot` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `charP` `RingHom.id`	—	`RingHom.ext` `expChar_prime` `charP` `ext` `RingHom.comp_apply` `RingHom.id_apply` `coeff_pthRoot` `coeff_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` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Perfection.commSemiring` `RingHom.instFunLike` `Perfection.coeff` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv`	—	`expChar_prime`
`comp_equiv'` 📖	mathematical	`PerfectionMap`	`RingHom.comp` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Perfection.commSemiring` `Perfection.coeff` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `equiv`	—	`expChar_prime` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`comp_map` 📖	mathematical	`PerfectionMap`	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `map`	—	`expChar_prime` `Equiv.symm_apply_apply`
`comp_symm_equiv` 📖	mathematical	`PerfectionMap`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingEquiv` `Ring.Perfection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Perfection.commSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `equiv` `Perfection.coeff`	—	`expChar_prime` `comp_equiv` `RingEquiv.apply_symm_apply`
`comp_symm_equiv'` 📖	mathematical	`PerfectionMap`	`RingHom.comp` `Ring.Perfection` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Perfection.commSemiring` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm` `equiv` `Perfection.coeff`	—	`expChar_prime` `RingHom.ext` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `comp_symm_equiv`
`equiv_apply` 📖	mathematical	`PerfectionMap`	`DFunLike.coe` `RingEquiv` `Ring.Perfection` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Perfection.commSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `equiv` `RingHom` `RingHom.instFunLike` `Equiv` `Equiv.instEquivLike` `Perfection.lift`	—	`expChar_prime`
`hom_ext` 📖	—	`PerfectionMap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	—	`expChar_prime` `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`	—	—	`expChar_prime`
`lift_apply` 📖	mathematical	`PerfectionMap`	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingHom.comp` `Ring.Perfection` `Perfection.commSemiring` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `RingEquiv.instEquivLike` `RingEquiv.symm` `equiv` `Perfection.lift`	—	`expChar_prime`
`lift_symm_apply` 📖	mathematical	`PerfectionMap`	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lift` `RingHom.comp`	—	`expChar_prime`
`map_eq_map` 📖	mathematical	—	`map` `Ring.Perfection` `Perfection.commSemiring` `Perfection.charP` `Perfection.perfectRing` `Perfection.coeff` `of` `Perfection.map`	—	`hom_ext` `Perfection.charP` `Perfection.perfectRing` `of` `map_map` `Perfection.coeff_map`
`map_map` 📖	mathematical	`PerfectionMap`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `map`	—	`expChar_prime` `RingHom.ext_iff` `comp_map`
`mk'` 📖	mathematical	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.Perfection` `Perfection.commSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Perfection.lift` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	`PerfectionMap`	—	`expChar_prime` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.injective` `RingHom.ext_iff` `Perfection.ext` `RingEquiv.surjective`
`of` 📖	mathematical	—	`PerfectionMap` `Ring.Perfection` `Perfection.commSemiring` `Perfection.charP` `Perfection.perfectRing` `Perfection.coeff`	—	`mk'` `Perfection.charP` `Perfection.perfectRing` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Equiv.apply_eq_iff_eq_symm_apply`
`surjective` 📖	mathematical	`PerfectionMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `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`	—	`expChar_prime`

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	29 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`, `pow_dvd_one_untiltAux_sub_one`, `WittVector.fontaineTheta_teichmuller`, `valAux_add`, `coeff_iterate_frobenius`, `valAux_one`, `untilt_iterate_frobeniusEquiv_symm_pow`, `instCharP`, `map_eq_zero`, `pow_dvd_mul_untiltAux_sub_untiltAux_mul`, `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` `Ring.Perfection` `Ideal.Quotient.commSemiring` `Perfection.commSemiring` `ModP.charP` `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.charP` `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.charP` `Perfection.coeff_frobeniusEquiv_symm`
`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.charP` `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.charP`
`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.charP` `Perfection.coeff_iterate_frobeniusEquiv_symm`
`coeff_nat_find_add_ne_zero` 📖	—	—	—	—	`Perfection.coeff_add_ne_zero` `ModP.charP` `Nat.find_spec`
`coeff_pow_p` 📖	mathematical	—	`ModP` `Monoid.toNatPow` `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.charP`
`instCharP` 📖	mathematical	—	`CharP` `PreTilt` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	`Perfection.charP` `ModP.charP`
`instPerfectRing` 📖	mathematical	—	`PerfectRing` `PreTilt` `CommRing.toCommSemiring` `instCommRing` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCharP`	—	`Perfection.perfectRing` `ModP.charP`
`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` `NNReal.instNoZeroDivisors`
`map_eq_zero` 📖	mathematical	`Valuation.Integers` `NNReal` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NNReal.instLinearOrderedCommGroupWithZero`	`DFunLike.coe` `Valuation` `PreTilt` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `CommRing.toRing` `instCommRing` `Valuation.instFunLike` `val` `instZeroNNReal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Valuation.map_zero` `Perfection.ext` `ModP.charP` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `NNReal.instNoZeroDivisors` `valAux_eq` `ModP.preVal_eq_zero`
`valAux_add` 📖	mathematical	`Valuation.Integers` `NNReal` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NNReal.instLinearOrderedCommGroupWithZero`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `valAux` `PreTilt` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `NNReal.instMax`	—	`zero_add` `valAux_zero` `max_eq_right` `zero_le` `NNReal.instCanonicallyOrderedAdd` `le_refl` `add_zero` `max_eq_left` `Perfection.ext` `ModP.charP` `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` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `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` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`MulZeroClass.zero_mul` `valAux_zero` `MulZeroClass.mul_zero` `Perfection.ext` `ModP.charP` `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` `instOneNNReal`	—	`valAux_eq` `one_ne_zero` `NeZero.one` `ModP.nontrivial` `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` `instZeroNNReal`	—	—

Ring

Definitions

Name	Category	Theorems
`Perfection` 📖	CompOp	28 math math: `Perfection.pthRoot_frobenius`, `Perfection.perfectRing`, `PerfectionMap.map_eq_map`, `Perfection.coeff_map`, `Perfection.charP`, `Perfection.coeff_mk`, `Perfection.coeff_iterate_frobenius`, `Perfection.map_apply_coe`, `PerfectionMap.comp_equiv'`, `Perfection.ext_iff`, `PerfectionMap.comp_equiv`, `PerfectionMap.comp_symm_equiv`, `Perfection.coeff_surjective`, `Perfection.coeff_pthRoot`, `Perfection.coeff_frobeniusEquiv_symm`, `Perfection.lift_apply_apply_coe`, `PerfectionMap.comp_symm_equiv'`, `Perfection.coeff_iterate_frobeniusEquiv_symm`, `Perfection.lift_symm_apply`, `PerfectionMap.of`, `Perfection.coeff_pow_p`, `Perfection.coeff_iterate_frobenius'`, `PerfectionMap.lift_apply`, `Perfection.coeff_pow_p'`, `PreTilt.coeff_def`, `PerfectionMap.equiv_apply`, `Perfection.frobenius_pthRoot`, `Perfection.coeff_frobenius`
`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`, `WittVector.ghostComponentModPPow_teichmuller_coeff`, `ModP.preVal_zero`, `PreTilt.coeff_iterate_frobenius`, `ModP.nontrivial`, `ModP.preVal_add`, `ModP.preVal_eq_zero`, `PreTilt.mk_untilt_eq_coeff_zero`, `WittVector.mk_fontaineTheta`, `PreTilt.coeff_def`, `PreTilt.coeff_iterate_frobenius'`, `ModP.charP`
`PerfectionMap` 📖	CompData	3 math math: `PerfectionMap.id`, `PerfectionMap.mk'`, `PerfectionMap.of`
`PreTilt` 📖	CompOp	29 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`, `PreTilt.pow_dvd_one_untiltAux_sub_one`, `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.pow_dvd_mul_untiltAux_sub_untiltAux_mul`, `PreTilt.mk_untilt_eq_coeff_zero`, `WittVector.mk_fontaineTheta`, `PreTilt.coeff_def`, `PreTilt.coeff_iterate_frobenius'`
`Tilt` 📖	CompOp	—

---

← Back to Index