Documentation Verification Report

TeichmullerSeries

📁 Source: Mathlib/RingTheory/WittVector/TeichmullerSeries.lean

Statistics

Metric	Count
Definitions	0
Theorems `dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff`, `eq_of_apply_teichmuller_eq`, `sum_coeff_eq_coeff_sum`, `teichmuller_mul_pow_coeff`, `teichmuller_mul_pow_coeff_of_ne`	5
Total	5

WittVector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff` 📖	mathematical	—	`WittVector` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRing` `hasNatPow` `instNatCast` `instSub` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `instMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidHom.instFunLike` `teichmuller` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `RingAut.instGroup` `RingEquiv.symm` `frobeniusEquiv` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `coeff`	—	`expChar_prime` `Ideal.mem_span_singleton` `mem_span_p_pow_iff_le_coeff_eq_zero` `le_coeff_eq_iff_le_sub_coeff_eq_zero` `sum_coeff_eq_coeff_sum` `Not.imp_symm` `teichmuller_mul_pow_coeff_of_ne` `Finset.sum_eq_add_sum_diff_singleton` `Finset.mem_Iic` `Finset.sum_congr` `RingAut.coe_pow` `teichmuller_mul_pow_coeff` `iterate_frobeniusEquiv_symm_pow_p_pow` `Finset.sum_const_zero` `add_zero`
`eq_of_apply_teichmuller_eq` 📖	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `instCommRing` `RingHom.instFunLike` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `teichmuller`	—	—	`expChar_prime` `RingHom.ext` `dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff` `Finset.sum_congr` `RingAut.coe_pow` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_sum` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_natCast` `sub_add_cancel` `pow_succ` `MulZeroClass.zero_mul` `zero_add`
`sum_coeff_eq_coeff_sum` 📖	mathematical	`Set.Elem` `setOf` `Finset` `Finset.instMembership` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Finset.sum` `WittVector` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instCommRing`	—	`Finset.induction` `zero_coeff` `Finset.subset_insert` `Finset.sum_insert` `Mathlib.Tactic.Push.not_forall_eq` `Function.mt` `Finset.sum_eq_zero` `Finset.mem_insert_self` `Finset.mem_insert_of_mem` `coeff_add_of_disjoint`
`teichmuller_mul_pow_coeff` 📖	mathematical	—	`coeff` `WittVector` `instMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `MonoidHom.instFunLike` `teichmuller` `hasNatPow` `instNatCast` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`zero_add` `mul_pow_charP_coeff_succ`
`teichmuller_mul_pow_coeff_of_ne` 📖	mathematical	—	`coeff` `WittVector` `instMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `MonoidHom.instFunLike` `teichmuller` `hasNatPow` `instNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`mul_pow_charP_coeff_zero` `LT.lt.le` `mul_pow_charP_coeff_succ` `teichmuller_coeff_pos` `zero_pow` `Nat.Prime.ne_zero` `Fact.out`

---

← Back to Index