Teichmuller

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

Statistics

Metric	Count
Definitions teichmuller, teichmullerFun	2
Theorems constantCoeff_surjective, ghostComponent_teichmuller, map_teichmuller, teichmuller_coeff_pos, teichmuller_coeff_zero, teichmuller_zero	6
Total	8

WittVector

Definitions

Name	Category	Theorems
teichmuller 📖	CompOp	11 math math: teichmuller_mul_pow_coeff_of_ne, map_teichmuller, teichmuller_zero, dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, fontaineThetaModPPow_teichmuller, ghostComponentModPPow_teichmuller_coeff, fontaineTheta_teichmuller, teichmuller_coeff_zero, teichmuller_mul_pow_coeff, teichmuller_coeff_pos, ghostComponent_teichmuller
teichmullerFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constantCoeff_surjective 📖	mathematical	—	WittVector DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike constantCoeff	—	—
ghostComponent_teichmuller 📖	mathematical	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike ghostComponent MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike teichmuller Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	—
map_teichmuller 📖	mathematical	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike map MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.instFunLike teichmuller	—	—
teichmuller_coeff_pos 📖	mathematical	—	coeff DFunLike.coe MonoidHom WittVector MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing MonoidHom.instFunLike teichmuller MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
teichmuller_coeff_zero 📖	mathematical	—	coeff DFunLike.coe MonoidHom WittVector MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing MonoidHom.instFunLike teichmuller	—	—
teichmuller_zero 📖	mathematical	—	DFunLike.coe MonoidHom WittVector MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing MonoidHom.instFunLike teichmuller MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instZero	—	ext zero_coeff

---

← Back to Index