Documentation Verification Report

Untilt

📁 Source: Mathlib/RingTheory/Perfectoid/Untilt.lean

Statistics

Metric	Count
Definitions `untilt`	1
Theorems `mk_comp_untilt_eq_coeff_zero`, `mk_untilt_eq_coeff_zero`, `untilt_iterate_frobeniusEquiv_symm_pow`	3
Total	4

PreTilt

Definitions

Name	Category	Theorems
`untilt` 📖	CompOp	6 math math: `mk_comp_untilt_eq_coeff_zero`, `WittVector.fontaineThetaModPPow_teichmuller`, `WittVector.ghostComponentModPPow_teichmuller_coeff`, `WittVector.fontaineTheta_teichmuller`, `untilt_iterate_frobeniusEquiv_symm_pow`, `mk_untilt_eq_coeff_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_comp_untilt_eq_coeff_zero` 📖	mathematical	—	`PreTilt` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `MonoidHom.instFunLike` `untilt` `ModP` `Ideal.Quotient.semiring` `coeff`	—	`Perfection.mk_comp_teichmuller'` `ModP.instCharPOfPrimeOfFactNotIsUnitCast`
`mk_untilt_eq_coeff_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `MonoidHom` `PreTilt` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `MonoidHom.instFunLike` `untilt` `ModP` `Ideal.Quotient.semiring` `coeff`	—	`Perfection.mk_teichmuller` `ModP.instCharPOfPrimeOfFactNotIsUnitCast`
`untilt_iterate_frobeniusEquiv_symm_pow` 📖	mathematical	—	`Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `MonoidHom` `PreTilt` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `instCommRing` `MonoidHom.instFunLike` `untilt` `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` `Nat.instMonoid`	—	`expChar_prime` `instCharP` `instPerfectRing` `MonoidHom.instMonoidHomClass` `iterate_frobeniusEquiv_symm_pow_p_pow`

---

← Back to Index