Teichmuller

📁 Source: Mathlib/RingTheory/Teichmuller.lean

Statistics

Metric	Count
Definitions quotientMulEquiv, teichmuller, teichmullerAux, teichmullerCauchy, teichmullerFun, teichmuller₀	6
Theorems coe_teichmuller_eq_teichmuller₀, coeff_quotientMulEquiv, coeff_zero_symm_quotientMulEquiv, exists_teichmullerFun, mk_comp_teichmuller, mk_comp_teichmuller', mk_comp_teichmuller₀, mk_teichmuller, mk_teichmuller₀, teichmullerAux_sModEq, teichmullerFun_eq_teichmuller₀, teichmullerFun_sModEq, teichmullerFun_spec, teichmullerFun_spec', teichmuller_eq_teichmuller₀_toMonoidHom, teichmuller_sModEq, teichmuller_spec, teichmuller_spec', teichmuller_zero, teichmuller₀_mapMonoidHom_idealQuotientMk, teichmuller₀_sModEq, teichmuller₀_spec, teichmuller₀_spec'	23
Total	29

Perfection

Definitions

Name	Category	Theorems
quotientMulEquiv 📖	CompOp	2 math math: coeff_quotientMulEquiv, coeff_zero_symm_quotientMulEquiv
teichmuller 📖	CompOp	9 math math: mk_teichmuller, mk_comp_teichmuller', teichmuller_sModEq, mk_comp_teichmuller, teichmuller_zero, coe_teichmuller_eq_teichmuller₀, teichmuller_eq_teichmuller₀_toMonoidHom, teichmuller_spec, teichmuller_spec'
teichmullerAux 📖	CompOp	2 math math: exists_teichmullerFun, teichmullerAux_sModEq
teichmullerCauchy 📖	CompOp	—
teichmullerFun 📖	CompOp	4 math math: teichmullerFun_spec', teichmullerFun_sModEq, teichmullerFun_spec, teichmullerFun_eq_teichmuller₀
teichmuller₀ 📖	CompOp	10 math math: mk_comp_teichmuller₀, teichmuller₀_spec, teichmuller₀_sModEq, teichmuller₀_spec', coe_teichmuller_eq_teichmuller₀, teichmuller_eq_teichmuller₀_toMonoidHom, mk_teichmuller₀, coeff_zero_symm_quotientMulEquiv, teichmuller₀_mapMonoidHom_idealQuotientMk, teichmullerFun_eq_teichmuller₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_teichmuller_eq_teichmuller₀ 📖	mathematical	—	DFunLike.coe MonoidHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller MonoidWithZeroHom MonoidWithZeroHom.funLike teichmuller₀	—	—
coeff_quotientMulEquiv 📖	mathematical	—	DFunLike.coe RingHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring Semiring.toNonAssocSemiring instCommSemiring RingHom.instFunLike coeff MulEquiv Ideal.Quotient.semiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid instCommMonoid CommRing.toCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Ideal.Quotient.commRing EquivLike.toFunLike MulEquiv.instEquivLike quotientMulEquiv Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 MonoidHom MonoidHom.instFunLike coeffMonoidHom	—	—
coeff_zero_symm_quotientMulEquiv 📖	mathematical	—	DFunLike.coe MonoidHom Perfection Monoid.toPow CommMonoid.toMonoid CommRing.toCommMonoid MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike coeffMonoidHom MulEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Ideal.Quotient.commRing MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm quotientMulEquiv MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀	—	coeffMonoidHom_zero_liftMonoidHom
exists_teichmullerFun 📖	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 Top.top Submodule.instTop teichmullerAux	—	IsPrecomplete.prec'
mk_comp_teichmuller 📖	mathematical	—	MonoidHom.comp Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHomClass.toMonoidHom RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass teichmuller coeff	—	MonoidHom.ext Ideal.instIsTwoSided_1 MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mk_teichmuller
mk_comp_teichmuller' 📖	mathematical	—	Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring Ring.toSemiring CommRing.toRing Ideal.instHasQuotient DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller coeff	—	Ideal.instIsTwoSided_1 mk_teichmuller
mk_comp_teichmuller₀ 📖	mathematical	—	MonoidWithZeroHom.comp Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHomClass.toMonoidWithZeroHom RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass teichmuller₀ coeff	—	MonoidWithZeroHom.ext Ideal.instIsTwoSided_1 RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mk_teichmuller
mk_teichmuller 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike MonoidHom Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller coeff	—	IsScalarTower.right teichmuller_sModEq Ideal.Quotient.mk_out Ideal.instIsTwoSided_1 pow_zero pow_one zero_add
mk_teichmuller₀ 📖	mathematical	—	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike MonoidWithZeroHom Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀ coeff	—	mk_teichmuller
teichmullerAux_sModEq 📖	mathematical	—	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id teichmullerAux	—	IsScalarTower.right pow_zero Ideal.one_eq_top teichmullerAux.congr_simp zero_add SModEq.symm teichmullerAux.eq_2 pow_succ' pow_mul SModEq.pow_pow_add_one Ideal.natCast_mem_of_charP_quotient Ideal.instIsTwoSided_1 map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Ideal.Quotient.mk_out coeff_pow_p'
teichmullerFun_eq_teichmuller₀ 📖	mathematical	—	teichmullerFun IsAdicComplete.toIsPrecomplete Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidWithZeroHom Perfection HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀	—	IsAdicComplete.toIsPrecomplete
teichmullerFun_sModEq 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id teichmullerFun Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid	—	Ideal.instIsTwoSided_1 IsScalarTower.right exists_teichmullerFun SModEq.trans SModEq.symm IsScalarTower.left Ideal.mul_top smul_eq_mul SModEq.pow_pow_add_one Ideal.natCast_mem_of_charP_quotient Ideal.Quotient.mk_out
teichmullerFun_spec 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	teichmullerFun IsAdicComplete.toIsPrecomplete Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.instIsTwoSided_1 IsScalarTower.right teichmullerFun_spec'
teichmullerFun_spec' 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	teichmullerFun IsAdicComplete.toIsPrecomplete Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.instIsTwoSided_1 IsScalarTower.right IsAdicComplete.toIsPrecomplete IsScalarTower.left IsHausdorff.eq_iff_smodEq IsAdicComplete.toIsHausdorff smul_eq_mul Ideal.mul_top le_total le_rfl SModEq.mono Ideal.pow_le_pow_right SModEq.trans teichmullerFun_sModEq
teichmuller_eq_teichmuller₀_toMonoidHom 📖	mathematical	—	teichmuller MonoidWithZeroHom.toMonoidHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring teichmuller₀	—	—
teichmuller_sModEq 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id DFunLike.coe MonoidHom Perfection HasQuotient.Quotient Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller Nat.instMonoid	—	Ideal.instIsTwoSided_1 teichmullerFun_sModEq IsAdicComplete.toIsPrecomplete
teichmuller_spec 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	DFunLike.coe MonoidHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller	—	Ideal.instIsTwoSided_1 IsScalarTower.right teichmullerFun_spec
teichmuller_spec' 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	DFunLike.coe MonoidHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller	—	Ideal.instIsTwoSided_1 IsScalarTower.right teichmullerFun_spec'
teichmuller_zero 📖	mathematical	—	DFunLike.coe MonoidHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidHom.instFunLike teichmuller MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Ideal.Quotient.commRing	—	Nat.Prime.ne_zero Fact.out teichmuller_spec Ideal.instIsTwoSided_1 IsScalarTower.right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_pow pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing
teichmuller₀_mapMonoidHom_idealQuotientMk 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀ MonoidHom CommMonoid.toMonoid CommRing.toCommMonoid Ideal.Quotient.commRing MulOneClass.toMulOne Monoid.toMulOneClass instCommMonoid MonoidHom.instFunLike mapMonoidHom MonoidHomClass.toMonoidHom RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coeffMonoidHom	—	teichmuller₀_spec Ideal.instIsTwoSided_1 MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.right coeffMonoidHom_pow_p_pow_self
teichmuller₀_sModEq 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff	SModEq CommRing.toRing Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Ideal Submodule.instPowNat IsScalarTower.right Algebra.id DFunLike.coe MonoidWithZeroHom Perfection HasQuotient.Quotient Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀ Nat.instMonoid	—	Ideal.instIsTwoSided_1 teichmullerFun_sModEq IsAdicComplete.toIsPrecomplete
teichmuller₀_spec 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	DFunLike.coe MonoidWithZeroHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀	—	Ideal.instIsTwoSided_1 IsScalarTower.right teichmullerFun_spec
teichmuller₀_spec' 📖	mathematical	DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Perfection CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.commSemiring instCommSemiring coeff SModEq Ring.toAddCommGroup Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Nat.instMonoid	DFunLike.coe MonoidWithZeroHom Perfection HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ideal.Quotient.semiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instCommSemiring Ideal.Quotient.commSemiring MonoidWithZeroHom.funLike teichmuller₀	—	Ideal.instIsTwoSided_1 IsScalarTower.right teichmullerFun_spec'

---

← Back to Index