Documentation Verification Report

Untilt

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

Statistics

Metric	Count
Definitions `untilt`, `untiltAux`, `untiltFun`	3
Theorems `exists_smodEq_untiltAux`, `mk_comp_untilt_eq_coeff_zero`, `mk_untilt_eq_coeff_zero`, `pow_dvd_mul_untiltAux_sub_untiltAux_mul`, `pow_dvd_one_untiltAux_sub_one`, `pow_dvd_untiltAux_sub_untiltAux`, `untiltAux_smodEq_untiltFun`, `untilt_iterate_frobeniusEquiv_symm_pow`	8
Total	11

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`
`untiltAux` 📖	CompOp	5 math math: `pow_dvd_untiltAux_sub_untiltAux`, `pow_dvd_one_untiltAux_sub_one`, `exists_smodEq_untiltAux`, `untiltAux_smodEq_untiltFun`, `pow_dvd_mul_untiltAux_sub_untiltAux_mul`
`untiltFun` 📖	CompOp	1 math math: `untiltAux_smodEq_untiltFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_smodEq_untiltAux` 📖	mathematical	—	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Submodule.instSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsScalarTower.right` `Algebra.id` `Submodule.instPowNat` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Top.top` `Submodule.instTop` `untiltAux`	—	`IsPrecomplete.prec'` `IsScalarTower.left` `IsScalarTower.right` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Ideal.mul_top` `pow_dvd_untiltAux_sub_untiltAux`
`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`	—	`Ideal.instIsTwoSided_1` `mk_untilt_eq_coeff_zero`
`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`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_out` `Ideal.Quotient.eq` `SModEq.sub_mem` `IsScalarTower.right` `IsAdicComplete.toIsPrecomplete` `pow_one` `pow_zero` `SModEq.symm` `untiltAux_smodEq_untiltFun`
`pow_dvd_mul_untiltAux_sub_untiltAux_mul` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `untiltAux` `PreTilt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `instCommRing`	—	`pow_zero` `mul_one` `sub_self` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `dvd_sub_pow_of_dvd_sub` `Ideal.mem_span_singleton` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq` `Ideal.Quotient.mk_out`
`pow_dvd_one_untiltAux_sub_one` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `untiltAux` `PreTilt` `AddMonoidWithOne.toOne` `instCommRing`	—	`pow_zero` `sub_self` `one_pow` `dvd_sub_pow_of_dvd_sub` `Ideal.mem_span_singleton` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Ideal.Quotient.mk_out`
`pow_dvd_untiltAux_sub_untiltAux` 📖	mathematical	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `untiltAux`	—	`pow_zero` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_add` `Nat.cast_one` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `pow_add` `pow_mul` `dvd_sub_pow_of_dvd_sub` `Ideal.mem_span_singleton` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq` `Ideal.Quotient.mk_out` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `expChar_prime` `instCharP` `coeff_iterate_frobenius'` `iterate_frobenius`
`untiltAux_smodEq_untiltFun` 📖	mathematical	—	`SModEq` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Ideal.span` `Set` `Set.instSingletonSet` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `untiltAux` `untiltFun`	—	`IsScalarTower.right` `exists_smodEq_untiltAux` `Ideal.mul_top` `Ideal.instIsTwoSided_1`
`untilt_iterate_frobeniusEquiv_symm_pow` 📖	mathematical	—	`Monoid.toNatPow` `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