LaurentSeries

📁 Source: Mathlib/RingTheory/LaurentSeries.lean

Statistics

Metric	Count
Definitions LaurentSeries, coeff, limit, LaurentSeriesAlgEquiv, LaurentSeriesPkg, LaurentSeriesRingEquiv, RatFuncAdicCompl, comparePkg, derivative, extensionAsRingHom, hasseDeriv, instAlgebraPowerSeries, instAlgebraRatFuncAdicCompl, instAlgebraSubtypeAdicCompletionPolynomialRatFuncIdealXMemValuationSubringAdicCompletionIntegers, instCoePowerSeries, instTopologicalSpaceSpaceRatFuncLaurentSeriesPkg, instUniformSpace, instUniformSpaceRatFuncAdicCompl, instValuedWithZeroMultiplicativeInt, powerSeriesAlgEquiv, powerSeriesEquivSubring, powerSeriesPart, powerSeriesRingEquiv, powerSeries_as_subring, ratfuncAdicComplPkg, ratfuncAdicComplRingEquiv, «term_⸨X⸩», idealX, coeToLaurentSeries	29
Theorems coeff_eventually_equal, coeff_support_bddBelow, coeff_tendsto, eventually_mem_nhds, exists_lb_coeff_ne, exists_lb_eventual_support, exists_lb_support, LaurentSeriesRingEquiv_def, LaurentSeriesRingEquiv_mem_valuationSubring, LaurentSeries_coe, X_order_mul_powerSeriesPart, algebraMap_C_mem_adicCompletionIntegers, algebraMap_apply, coe_X_compare, coe_algebraMap, coe_range_dense, coeff_coe_powerSeries, coeff_zero_of_lt_intValuation, coeff_zero_of_lt_valuation, comparePkg_eq_extension, continuous_coe, derivative_apply, derivative_iterate, derivative_iterate_coeff, eq_coeff_of_valuation_sub_lt, exists_Polynomial_intValuation_lt, exists_powerSeries_of_memIntegers, exists_ratFunc_eq_v, exists_ratFunc_val_lt, hasseDeriv_coeff, hasseDeriv_comp, hasseDeriv_comp_coeff, hasseDeriv_single, hasseDeriv_single_add, hasseDeriv_zero, inducing_coe, instIsFractionRingPowerSeries, instLaurentSeriesComplete, intValuation_le_iff_coeff_lt_eq_zero, mem_integers_of_powerSeries, ofPowerSeries_powerSeriesPart, of_powerSeries_localization, powerSeriesEquivSubring_apply, powerSeriesEquivSubring_coe_apply, powerSeriesPart_coeff, powerSeriesPart_eq_zero, powerSeriesPart_zero, powerSeriesRingEquiv_coe_apply, powerSeries_ext_subring, ratfuncAdicComplRingEquiv_apply, single_order_mul_powerSeriesPart, tendsto_valuation, uniformContinuous_coeff, val_le_one_iff_eq_coe, valuation_LaurentSeries_equal_extension, valuation_X_pow, valuation_coe_ratFunc, valuation_compare, valuation_def, valuation_le_iff_coeff_lt_eq_zero, valuation_le_iff_coeff_lt_log_eq_zero, valuation_single_zpow, coe_C, coe_X, coe_add, coe_mul, coe_neg, coe_one, coe_pow, coe_smul, coe_sub, coe_zero, coeff_coe, intValuation_X, intValuation_eq_of_coe, algebraMap_apply_div, coe_X, coe_coe, instFaithfulSMulPolynomialLaurentSeries, single_inv, single_one_eq_pow, single_zpow, valuation_eq_LaurentSeries_valuation	83
Total	112

LaurentSeries

Definitions

Name	Category	Theorems
LaurentSeriesAlgEquiv 📖	CompOp	—
LaurentSeriesPkg 📖	CompOp	5 math math: LaurentSeriesRingEquiv_def, valuation_LaurentSeries_equal_extension, LaurentSeries_coe, valuation_compare, ratfuncAdicComplRingEquiv_apply
LaurentSeriesRingEquiv 📖	CompOp	7 math math: LaurentSeriesRingEquiv_def, algebraMap_C_mem_adicCompletionIntegers, exists_powerSeries_of_memIntegers, LaurentSeriesRingEquiv_mem_valuationSubring, powerSeries_ext_subring, powerSeriesRingEquiv_coe_apply, mem_integers_of_powerSeries
RatFuncAdicCompl 📖	CompOp	10 math math: LaurentSeriesRingEquiv_def, algebraMap_C_mem_adicCompletionIntegers, coe_X_compare, LaurentSeriesRingEquiv_mem_valuationSubring, powerSeries_ext_subring, powerSeriesRingEquiv_coe_apply, valuation_compare, comparePkg_eq_extension, ratfuncAdicComplRingEquiv_apply, mem_integers_of_powerSeries
comparePkg 📖	CompOp	1 math math: comparePkg_eq_extension
derivative 📖	CompOp	3 math math: derivative_iterate_coeff, derivative_apply, derivative_iterate
extensionAsRingHom 📖	CompOp	1 math math: comparePkg_eq_extension
hasseDeriv 📖	CompOp	8 math math: derivative_apply, hasseDeriv_comp_coeff, hasseDeriv_coeff, hasseDeriv_single_add, hasseDeriv_comp, derivative_iterate, hasseDeriv_zero, hasseDeriv_single
instAlgebraPowerSeries 📖	CompOp	5 math math: coe_algebraMap, of_powerSeries_localization, RatFunc.valuation_eq_LaurentSeries_valuation, valuation_def, instIsFractionRingPowerSeries
instAlgebraRatFuncAdicCompl 📖	CompOp	—
instAlgebraSubtypeAdicCompletionPolynomialRatFuncIdealXMemValuationSubringAdicCompletionIntegers 📖	CompOp	—
instCoePowerSeries 📖	CompOp	—
instTopologicalSpaceSpaceRatFuncLaurentSeriesPkg 📖	CompOp	—
instUniformSpace 📖	CompOp	1 math math: comparePkg_eq_extension
instUniformSpaceRatFuncAdicCompl 📖	CompOp	2 math math: tendsto_valuation, comparePkg_eq_extension
instValuedWithZeroMultiplicativeInt 📖	CompOp	18 math math: valuation_le_iff_coeff_lt_eq_zero, valuation_single_zpow, inducing_coe, continuous_coe, val_le_one_iff_eq_coe, exists_ratFunc_val_lt, intValuation_le_iff_coeff_lt_eq_zero, valuation_LaurentSeries_equal_extension, instLaurentSeriesComplete, valuation_coe_ratFunc, valuation_compare, coe_range_dense, comparePkg_eq_extension, valuation_def, valuation_le_iff_coeff_lt_log_eq_zero, uniformContinuous_coeff, exists_ratFunc_eq_v, valuation_X_pow
powerSeriesAlgEquiv 📖	CompOp	—
powerSeriesEquivSubring 📖	CompOp	2 math math: powerSeriesEquivSubring_apply, powerSeriesEquivSubring_coe_apply
powerSeriesPart 📖	CompOp	6 math math: ofPowerSeries_powerSeriesPart, single_order_mul_powerSeriesPart, powerSeriesPart_coeff, X_order_mul_powerSeriesPart, powerSeriesPart_zero, powerSeriesPart_eq_zero
powerSeriesRingEquiv 📖	CompOp	1 math math: powerSeriesRingEquiv_coe_apply
powerSeries_as_subring 📖	CompOp	3 math math: powerSeries_ext_subring, powerSeriesEquivSubring_apply, powerSeriesEquivSubring_coe_apply
ratfuncAdicComplPkg 📖	CompOp	3 math math: LaurentSeriesRingEquiv_def, valuation_compare, ratfuncAdicComplRingEquiv_apply
ratfuncAdicComplRingEquiv 📖	CompOp	2 math math: coe_X_compare, ratfuncAdicComplRingEquiv_apply
«term_⸨X⸩» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LaurentSeriesRingEquiv_def 📖	mathematical	—	DFunLike.coe RingEquiv LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain RatFuncAdicCompl HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing UniformSpace.Completion.mul WithVal RatFunc WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX WithVal.instRing Valued.toUniformSpace WithVal.instValued HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike LaurentSeriesRingEquiv RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries AbstractCompletion.compare instIsDomain Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt LaurentSeriesPkg ratfuncAdicComplPkg	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
LaurentSeriesRingEquiv_mem_valuationSubring 📖	mathematical	—	RatFuncAdicCompl ValuationSubring UniformSpace.Completion.instField WithVal RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike Valuation.valuationSubring Valued.v Valued.valuedCompletion DFunLike.coe RingEquiv LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing UniformSpace.Completion.mul HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike LaurentSeriesRingEquiv RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries	—	Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid LaurentSeriesRingEquiv_def IsTopologicalDivisionRing.toIsTopologicalRing valuation_compare val_le_one_iff_eq_coe
LaurentSeries_coe 📖	mathematical	—	AbstractCompletion.coe RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt LaurentSeriesPkg DFunLike.coe RingHom LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring HahnSeries.instSemiring instLatticeInt DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Int.instSemiring Int.instIsStrictOrderedRing Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries	—	instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
X_order_mul_powerSeriesPart 📖	mathematical	HahnSeries.order SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	DFunLike.coe RingHom PowerSeries HahnSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing MvPowerSeries.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.X powerSeriesPart	—	Int.instIsStrictOrderedRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass HahnSeries.ofPowerSeries_X HahnSeries.single_pow nsmul_eq_mul mul_one one_pow single_order_mul_powerSeriesPart
algebraMap_C_mem_adicCompletionIntegers 📖	mathematical	—	RatFuncAdicCompl ValuationSubring IsDedekindDomain.HeightOneSpectrum.adicCompletion Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc RatFunc.instField RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial Polynomial.idealX UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.comp LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instNonAssocSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing RingEquiv.toRingHom LaurentSeriesRingEquiv HahnSeries.C	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.ofPowerSeries_C IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass LaurentSeriesRingEquiv_mem_valuationSubring
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield HahnSeries.instSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap HahnSeries.powerSeriesAlgebra PowerSeries.instAlgebra Algebra.id HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring HahnSeries.instNonAssocSemiring HahnSeries.C	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.ofPowerSeries_C
coe_X_compare 📖	mathematical	—	DFunLike.coe RingEquiv RatFuncAdicCompl LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain UniformSpace.Completion.mul WithVal RatFunc WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX WithVal.instRing Valued.toUniformSpace WithVal.instValued HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid EquivLike.toFunLike RingEquiv.instEquivLike ratfuncAdicComplRingEquiv UniformSpace.Completion.coe' RatFunc.X instIsDomain RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries PowerSeries.X	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain PowerSeries.coe_X Int.instIsOrderedAddMonoid RatFunc.instFaithfulSMulPolynomialLaurentSeries RatFunc.coe_X Multiplicative.isOrderedMonoid LaurentSeries_coe AbstractCompletion.compare_coe
coe_algebraMap 📖	mathematical	—	DFunLike.coe RingHom PowerSeries LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring PowerSeries.instCommSemiring HahnSeries.instSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing RingHom.instFunLike algebraMap instAlgebraPowerSeries HahnSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid HahnSeries.ofPowerSeries	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_range_dense 📖	mathematical	—	DenseRange LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain UniformSpace.toTopologicalSpace Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid instValuedWithZeroMultiplicativeInt RatFunc DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RatFunc.instField HahnSeries.instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid RatFunc.instFaithfulSMulPolynomialLaurentSeries denseRange_iff_closure_range Set.ext uniformity_eq_comap_neg_add_nhds_zero_swapped IsUniformAddGroup.isLeftUniformAddGroup Valued.toIsUniformAddGroup Valued.mem_nhds_zero exists_ratFunc_val_lt add_comm
coeff_coe_powerSeries 📖	mathematical	—	HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom PowerSeries HahnSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing LinearMap RingHom.id PowerSeries.instAddCommMonoid PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff	—	Int.instIsStrictOrderedRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid HahnSeries.ofPowerSeries_apply_coeff
coeff_zero_of_lt_intValuation 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation HahnSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt RingHom PowerSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries WithZero.exp	LinearMap RingHom.id PowerSeries.instAddCommMonoid PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing PowerSeries.X_pow_dvd_iff IsScalarTower.right span_singleton_dvd_span_singleton_iff_dvd PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing IsScalarTower.left Ideal.span_singleton_pow Ideal.instIsTwoSided_1 PowerSeries.idealX.eq_1 Multiplicative.isOrderedCancelMonoid IsPrincipalIdealRing.isDedekindDomain IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd instIsFractionRingPowerSeries IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap valuation_def coe_algebraMap
coeff_zero_of_lt_valuation 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt WithZero.exp	HahnSeries.coeff	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.coeff_eq_zero_of_lt_order neg_le_iff_add_nonneg covariant_swap_add_of_covariant_add Int.instAddLeftMono eq_add_neg_of_add_eq add_comm powerSeriesPart_coeff intValuation_le_iff_coeff_lt_eq_zero ofPowerSeries_powerSeriesPart neg_neg neg_add_rev WithZero.exp_add map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass HahnSeries.ofPowerSeries_X_pow PowerSeries.coe_pow valuation_X_pow mul_le_mul_right WithZero.instMulLeftMono IsOrderedMonoid.toMulLeftMono lt_of_not_ge 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.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing neg_eq_zero sub_eq_zero_of_eq le_of_lt sub_eq_iff_eq_add neg_sub sub_eq_add_neg valuation_single_zpow
comparePkg_eq_extension 📖	mathematical	—	Equiv.toFun RatFuncAdicCompl LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain UniformEquiv.toEquiv instUniformSpaceRatFuncAdicCompl instUniformSpace comparePkg OneHom.toFun UniformSpace.Completion RatFunc Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing MonoidHom.toOneHom RingHom.toMonoidHom extensionAsRingHom continuous_coe instLaurentSeriesComplete CompletableTopField.toT0Space HahnSeries.instField Valued.completable instValuedWithZeroMultiplicativeInt	—	instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid
continuous_coe 📖	mathematical	—	Continuous RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing UniformSpace.toTopologicalSpace Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instValuedWithZeroMultiplicativeInt DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring HahnSeries.instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries	—	UniformContinuous.continuous instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RatFunc.instFaithfulSMulPolynomialLaurentSeries isUniformInducing_iff' inducing_coe
derivative_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike derivative hasseDeriv	—	—
derivative_iterate 📖	mathematical	—	Nat.iterate LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike derivative AddMonoid.toNatSMul HahnSeries.instAddMonoid SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid Nat.factorial hasseDeriv	—	HahnSeries.ext hasseDeriv_zero one_smul Function.iterate_succ derivative_apply hasseDeriv_comp Nat.choose_symm_add Nat.choose_one_right Nat.factorial.eq_2 mul_nsmul
derivative_iterate_coeff 📖	mathematical	—	HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Nat.iterate LaurentSeries DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring HahnSeries.instAddCommMonoid AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike derivative SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Polynomial.smeval Ring.toSemiring Int.instRing descPochhammer Int.instAddCommMonoid Monoid.toNatPow Int.instMonoid MonoidWithZero.toMulActionWithZero Semiring.toMonoidWithZero	—	derivative_iterate HahnSeries.coeff_nsmul Pi.smul_apply hasseDeriv_coeff Ring.descPochhammer_eq_factorial_smul_choose Monoid.PowAssoc smul_assoc AddCommMonoid.nat_isScalarTower
eq_coeff_of_valuation_sub_lt 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt HahnSeries.instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup WithZero.exp	HahnSeries.coeff	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing eq_of_sub_eq_zero HahnSeries.coeff_sub coeff_zero_of_lt_valuation
exists_Polynomial_intValuation_lt 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation PowerSeries WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing PowerSeries.instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.intValuation IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain DivisionRing.toRing Field.toDivisionRing instIsDomain Field.toSemifield IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing PowerSeries.idealX SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.toPowerSeries DivisionSemiring.toSemiring Semifield.toDivisionSemiring Units.val MonoidWithZero.toMonoid WithZero.instMonoidWithZero Multiplicative.monoid Int.instAddMonoid	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing sub_zero LE.le.trans_lt IsDedekindDomain.HeightOneSpectrum.intValuation_le_one Units.ne_zero WithZero.instNontrivial toAdd_one Multiplicative.toAdd_le WithZero.coe_le_coe WithZero.coe_unzero WithZero.coe_one Units.val_one Units.val_le_val Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid intValuation_le_iff_coeff_lt_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Polynomial.coeff_coe PowerSeries.coeff_trunc instIsFractionRingPowerSeries IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap lt_of_le_of_lt coe_algebraMap WithZero.coe_mul ofAdd_toAdd ofAdd_add neg_add mul_one mul_assoc one_mul mul_lt_mul_of_pos_left LinearOrderedCommMonoidWithZero.toPosMulStrictMono WithZero.coe_lt_coe ofAdd_neg Right.inv_lt_one_iff IsRightCancelMul.mulRightStrictMono_of_mulRightMono Multiplicative.isRightCancelMul AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ofAdd_zero Multiplicative.ofAdd_lt zero_lt_iff
exists_powerSeries_of_memIntegers 📖	mathematical	RatFuncAdicCompl ValuationSubring IsDedekindDomain.HeightOneSpectrum.adicCompletion Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc RatFunc.instField RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial Polynomial.idealX UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers	DFunLike.coe RingEquiv LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing UniformSpace.Completion.mul HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike LaurentSeriesRingEquiv RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries	—	IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid AbstractCompletion.inverse_compare val_le_one_iff_eq_coe IsTopologicalDivisionRing.toIsTopologicalRing IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers valuation_compare RingEquiv.symm_apply_apply
exists_ratFunc_eq_v 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v RatFunc.instValuedWithZeroMultiplicativeInt LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instValuedWithZeroMultiplicativeInt	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instIsDomain IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing map_zero Multiplicative.isOrderedCancelMonoid MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial zpow_neg map_inv₀ map_zpow₀ RatFunc.v_def Polynomial.valuation_X_eq_neg_one WithZero.exp_zsmul WithZero.exp_neg mul_neg mul_one neg_neg WithZero.exp_log
exists_ratFunc_val_lt 📖	mathematical	—	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt HahnSeries.instSub AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup RingHom RatFunc Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RatFunc.instField HahnSeries.instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries Units.val MonoidWithZero.toMonoid WithZero.instMonoidWithZero Multiplicative.monoid Int.instAddMonoid	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RatFunc.instFaithfulSMulPolynomialLaurentSeries WithZero.coe_ne_zero Multiplicative.isOrderedCancelMonoid IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing exists_Polynomial_intValuation_lt ofPowerSeries_powerSeriesPart le_of_lt algebraMap.coe_one inv_mul_eq_iff_eq_mul₀ PowerSeries.coe_pow PowerSeries.coe_X isReduced_of_noZeroDivisors HahnSeries.instNoZeroDivisors IsDomain.to_noZeroDivisors NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing HahnSeries.ofPowerSeries_X_pow neg_neg map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass zpow_neg zpow_natCast inv_eq_one_div map_div₀ RingHomClass.toMonoidWithZeroHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RatFunc.coe_X map_one MonoidHomClass.toOneHomClass mul_sub MonoidHomClass.toMulHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_inv₀ valuation_X_pow RatFunc.coe_coe PowerSeries.coe_sub coe_algebraMap instIsFractionRingPowerSeries IsDedekindDomain.HeightOneSpectrum.adicValued_apply IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap WithZero.exp_ne_zero Units.val_mk0 inv_mul_lt_of_lt_mul₀ Units.val_mul X_order_mul_powerSeriesPart
hasseDeriv_coeff 📖	mathematical	—	HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries HahnSeries.instAddCommMonoid AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike hasseDeriv SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Int.instCommRing Monoid.toNatPow Int.instMonoid Int.instBinomialRing	—	—
hasseDeriv_comp 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike hasseDeriv AddMonoid.toNatSMul HahnSeries.instAddMonoid SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid Nat.choose	—	HahnSeries.ext hasseDeriv_comp_coeff Nat.cast_add
hasseDeriv_comp_coeff 📖	mathematical	—	HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries HahnSeries.instAddCommMonoid AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike hasseDeriv AddMonoid.toNatSMul HahnSeries.instAddMonoid SubNegMonoid.toAddMonoid SubNegZeroMonoid.toSubNegMonoid Nat.choose	—	HahnSeries.coeff_nsmul Nat.cast_add smul_smul mul_comm Ring.choose_add_smul_choose Monoid.PowAssoc add_assoc Nat.choose_symm_add smul_assoc AddCommMonoid.nat_isScalarTower
hasseDeriv_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike hasseDeriv ZeroHom HahnSeries HahnSeries.instZero ZeroHom.funLike HahnSeries.single SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Int.instCommRing Monoid.toNatPow Int.instMonoid Int.instBinomialRing	—	hasseDeriv_single_add
hasseDeriv_single_add 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule LinearMap.instFunLike hasseDeriv ZeroHom HahnSeries HahnSeries.instZero ZeroHom.funLike HahnSeries.single SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.choose NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Int.instCommRing Monoid.toNatPow Int.instMonoid Int.instBinomialRing	—	HahnSeries.ext HahnSeries.coeff_single_same HahnSeries.coeff_single_of_ne smul_zero
hasseDeriv_zero 📖	mathematical	—	hasseDeriv LinearMap.id LaurentSeries NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HahnSeries.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt AddCommGroup.toAddCommMonoid HahnSeries.instModule	—	LinearMap.ext HahnSeries.ext CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero add_zero Ring.choose_zero_right' pow_zero one_smul
inducing_coe 📖	mathematical	—	IsUniformInducing RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instValuedWithZeroMultiplicativeInt DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring HahnSeries.instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries	—	instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RatFunc.instFaithfulSMulPolynomialLaurentSeries isUniformInducing_iff Filter.comap.eq_1 Filter.ext uniformity_eq_comap_nhds_zero IsUniformAddGroup.isRightUniformAddGroup Valued.toIsUniformAddGroup Valued.mem_nhds sub_zero subset_refl Set.instReflSubset subset_trans Set.instIsTransSubset map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing instIsFractionRingPowerSeries valuation_def Multiplicative.isOrderedCancelMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial RatFunc.valuation_eq_LaurentSeries_valuation Set.Subset.refl Set.mem_setOf_eq RatFunc.v_def
instIsFractionRingPowerSeries 📖	mathematical	—	IsFractionRing PowerSeries PowerSeries.instCommSemiring Semifield.toCommSemiring Field.toSemifield LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain HahnSeries.instCommSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instAlgebraPowerSeries	—	IsLocalization.of_le IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing of_powerSeries_localization powers_le_nonZeroDivisors_of_noZeroDivisors PowerSeries.instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain PowerSeries.X_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing isUnit_of_mem_nonZeroDivisors Int.instIsOrderedAddMonoid map_mem_nonZeroDivisors PowerSeries.instNontrivial HahnSeries.instNoZeroDivisors MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass HahnSeries.ofPowerSeries_injective
instLaurentSeriesComplete 📖	mathematical	—	CompleteSpace LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid instValuedWithZeroMultiplicativeInt	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Cauchy.eventually_mem_nhds
intValuation_le_iff_coeff_lt_eq_zero 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation HahnSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt RingHom PowerSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries WithZero.exp LinearMap RingHom.id PowerSeries.instAddCommMonoid PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	PowerSeries.X_pow_dvd_iff Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing coe_algebraMap IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing instIsFractionRingPowerSeries valuation_def Multiplicative.isOrderedCancelMonoid IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap IsScalarTower.right span_singleton_dvd_span_singleton_iff_dvd IsScalarTower.left Ideal.span_singleton_pow Ideal.instIsTwoSided_1 IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd
mem_integers_of_powerSeries 📖	mathematical	—	RatFuncAdicCompl ValuationSubring IsDedekindDomain.HeightOneSpectrum.adicCompletion Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc RatFunc.instField RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial Polynomial.idealX UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers DFunLike.coe RingEquiv LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing UniformSpace.Completion.mul HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike LaurentSeriesRingEquiv RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries	—	IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsTopologicalDivisionRing.toIsTopologicalRing valuation_compare
ofPowerSeries_powerSeriesPart 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RingHom.instFunLike HahnSeries.ofPowerSeries powerSeriesPart LaurentSeries HahnSeries.instMul Int.instAddCommMonoid ZeroHom HahnSeries.instZero ZeroHom.funLike HahnSeries.single HahnSeries.order NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing mul_assoc HahnSeries.single_mul_single neg_add_cancel mul_one HahnSeries.C_apply HahnSeries.C_one one_mul single_order_mul_powerSeriesPart
of_powerSeries_localization 📖	mathematical	—	IsLocalization PowerSeries PowerSeries.instCommSemiring CommRing.toCommSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerSeries.instSemiring CommSemiring.toSemiring PowerSeries.X LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instCommSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instAlgebraPowerSeries	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.single_mul_single add_neg_cancel mul_one neg_add_cancel HahnSeries.ofPowerSeries_X_pow map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass single_order_mul_powerSeriesPart ofPowerSeries_powerSeriesPart mul_comm LT.lt.le coe_algebraMap HahnSeries.ofPowerSeries_injective
powerSeriesEquivSubring_apply 📖	mathematical	—	DFunLike.coe RingEquiv PowerSeries LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing SetLike.instMembership Subring.instSetLike powerSeries_as_subring MvPowerSeries.instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Subring.toCommRing HahnSeries.instCommRing Distrib.toAdd PowerSeries.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike powerSeriesEquivSubring RingHom HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries Subring.map PowerSeries.instRing DivisionRing.toRing Field.toDivisionRing Top.top Subring.instTop Ring.toSemiring Subring.mem_map	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
powerSeriesEquivSubring_coe_apply 📖	mathematical	—	LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subring HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing SetLike.instMembership Subring.instSetLike powerSeries_as_subring DFunLike.coe RingEquiv PowerSeries MvPowerSeries.instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Subring.toCommRing HahnSeries.instCommRing Distrib.toAdd PowerSeries.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike powerSeriesEquivSubring RingHom HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
powerSeriesPart_coeff 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff powerSeriesPart HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass HahnSeries.order NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
powerSeriesPart_eq_zero 📖	mathematical	—	powerSeriesPart PowerSeries PowerSeries.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LaurentSeries HahnSeries.instZero SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	Mathlib.Tactic.Contrapose.contrapose₁ PowerSeries.ext_iff powerSeriesPart_coeff CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero add_zero PowerSeries.coeff_zero_eq_constantCoeff powerSeriesPart_zero
powerSeriesPart_zero 📖	mathematical	—	powerSeriesPart LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries.instZero SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt PowerSeries PowerSeries.instZero	—	PowerSeries.ext powerSeriesPart_coeff HahnSeries.order_zero zero_add LinearMap.map_zero
powerSeriesRingEquiv_coe_apply 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.adicCompletion Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc RatFunc.instField RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial Polynomial.idealX ValuationSubring UniformSpace.Completion.instField WithVal WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder IsDedekindDomain.HeightOneSpectrum.valuation WithVal.instField Valued.toUniformSpace WithVal.instRing WithVal.instValued Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup SetLike.instMembership ValuationSubring.instSetLike IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers DFunLike.coe RingEquiv PowerSeries MvPowerSeries.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ValuationSubring.instCommRingSubtypeMem Distrib.toAdd PowerSeries.instCommRing EquivLike.toFunLike RingEquiv.instEquivLike powerSeriesRingEquiv LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass RatFuncAdicCompl HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing UniformSpace.Completion.mul HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCompletion WithVal.instCommRing RatFunc.instCommRing LaurentSeriesRingEquiv RingHom HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PowerSeries.instSemiring HahnSeries.instNonAssocSemiring RingHom.instFunLike HahnSeries.ofPowerSeries	—	IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial Valued.isTopologicalDivisionRing Valued.completable Valued.toIsUniformAddGroup
powerSeries_ext_subring 📖	mathematical	—	Subring.map LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain RatFuncAdicCompl HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing UniformSpace.Completion.ring WithVal RatFunc WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX WithVal.instRing Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing WithVal.instField UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup RingEquiv.toRingHom HahnSeries.instNonAssocSemiring Semiring.toNonAssocSemiring UniformSpace.Completion.instField Valued.completable LaurentSeriesRingEquiv powerSeries_as_subring ValuationSubring.toSubring IsDedekindDomain.HeightOneSpectrum.adicCompletion IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc.instIsFractionRingPolynomial IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers	—	Subring.ext IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valued.completable IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial mem_integers_of_powerSeries exists_powerSeries_of_memIntegers
ratfuncAdicComplRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv RatFuncAdicCompl LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain UniformSpace.Completion.mul WithVal RatFunc WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX WithVal.instRing Valued.toUniformSpace WithVal.instValued HahnSeries.instMul Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing instAddCompletion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib WithVal.instCommRing RatFunc.instCommRing HahnSeries.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid EquivLike.toFunLike RingEquiv.instEquivLike ratfuncAdicComplRingEquiv AbstractCompletion.compare instIsDomain Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt ratfuncAdicComplPkg LaurentSeriesPkg	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
single_order_mul_powerSeriesPart 📖	mathematical	—	HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries.instMul Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DFunLike.coe ZeroHom HahnSeries.instZero ZeroHom.funLike HahnSeries.single HahnSeries.order NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne RingHom PowerSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries powerSeriesPart	—	HahnSeries.ext IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing sub_add_cancel HahnSeries.coeff_single_mul_add one_mul sub_nonneg_of_le covariant_swap_add_of_covariant_add Int.instAddLeftMono coeff_coe_powerSeries powerSeriesPart_coeff add_sub_cancel StrictMono.injective Nat.strictMono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero Nat.instIsOrderedCancelAddMonoid HahnSeries.ofPowerSeries_apply HahnSeries.embDomain_notin_range Mathlib.Tactic.Contrapose.contrapose₄ Mathlib.Tactic.Contrapose.contrapose₂ HahnSeries.order_le_of_coeff_ne_zero
tendsto_valuation 📖	mathematical	—	Filter.Tendsto RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v RatFunc.instValuedWithZeroMultiplicativeInt Filter.comap IsDedekindDomain.HeightOneSpectrum.adicCompletion Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.commRing IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial Polynomial.idealX UniformSpace.Completion.coe' WithVal IsDedekindDomain.HeightOneSpectrum.valuation Valued.toUniformSpace WithVal.instRing WithVal.instValued nhds UniformSpace.toTopologicalSpace instUniformSpaceRatFuncAdicCompl WithZeroTopology.topologicalSpace UniformSpace.Completion.ring IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valued.valuedCompletion	—	IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valued.is_topological_valuation Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Filter.tendsto_def Filter.HasBasis.mem_iff' WithZeroTopology.hasBasis_nhds_zero map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Units.val_mk0 subset_refl Set.instReflSubset Set.Subset.trans Set.mem_preimage Set.mem_Iio Valued.valuedCompletion_apply Set.preimage_mono Valued.completable WithZeroTopology.tendsto_of_ne_zero Valuation.ne_zero_iff WithZero.instNontrivial Filter.eventually_comap Filter.Eventually.eq_1 Valued.mem_nhds Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Valuation.map_eq_of_sub_lt
uniformContinuous_coeff 📖	mathematical	—	UniformContinuous LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid instValuedWithZeroMultiplicativeInt HahnSeries.coeff	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid uniformContinuous_iff_eventually Filter.eventually_iff_exists_mem WithZero.coe_ne_zero Filter.HasBasis.mem_of_mem Valued.hasBasis_uniformity eq_coeff_of_valuation_sub_lt le_of_lt lt_add_one Int.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono mem_uniformity_of_eq
val_le_one_iff_eq_coe 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt WithZero.one instOneMultiplicativeOfZero Int.instCommRing RingHom PowerSeries HahnSeries NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuation_le_iff_coeff_lt_log_eq_zero one_ne_zero NeZero.one WithZero.instNontrivial WithZero.log_one neg_zero HahnSeries.ext coeff_coe_powerSeries HahnSeries.embDomain_notin_range Nat.instIsOrderedCancelAddMonoid
valuation_LaurentSeries_equal_extension 📖	mathematical	—	IsDenseInducing.extend RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain AbstractCompletion.space Valued.toUniformSpace DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt LaurentSeriesPkg UniformSpace.toTopologicalSpace AbstractCompletion.uniformStruct AbstractCompletion.coe WithZeroTopology.topologicalSpace AbstractCompletion.isDenseInducing DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero Valuation.instFunLike Valued.v LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instValuedWithZeroMultiplicativeInt	—	IsDenseInducing.extend_unique instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing AbstractCompletion.isDenseInducing Multiplicative.isOrderedCancelMonoid IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial RatFunc.v_def PowerSeries.instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing instIsFractionRingPowerSeries RatFunc.instFaithfulSMulPolynomialLaurentSeries RatFunc.valuation_eq_LaurentSeries_valuation Valued.continuous_valuation
valuation_X_pow 📖	mathematical	—	DFunLike.coe Valuation HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring RingHom PowerSeries PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid RingHom.instFunLike HahnSeries.ofPowerSeries PowerSeries.X WithZero.exp	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing map_pow MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing instIsFractionRingPowerSeries valuation_def coe_algebraMap Multiplicative.isOrderedCancelMonoid IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap PowerSeries.intValuation_X WithZero.exp_nsmul smul_neg nsmul_one
valuation_coe_ratFunc 📖	mathematical	—	DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt RingHom RatFunc Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RatFunc.instField HahnSeries.instSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap RatFunc.liftAlgebra HahnSeries.instField HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id RatFunc.instFaithfulSMulPolynomialLaurentSeries DivisionRing.toRing Field.toDivisionRing instIsDomain RatFunc.instValuedWithZeroMultiplicativeInt	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RatFunc.instFaithfulSMulPolynomialLaurentSeries Multiplicative.isOrderedCancelMonoid instIsDomain IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial
valuation_compare 📖	mathematical	—	DFunLike.coe Valuation RatFuncAdicCompl WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder UniformSpace.Completion.ring WithVal RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing RatFunc.instField IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commRing RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id Polynomial.idealX Valued.toUniformSpace WithVal.instValued IsTopologicalDivisionRing.toIsTopologicalRing UniformSpace.toTopologicalSpace Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup Valuation.instFunLike Valued.v Valued.valuedCompletion AbstractCompletion.compare instIsDomain Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid RatFunc.instValuedWithZeroMultiplicativeInt LaurentSeriesPkg ratfuncAdicComplPkg LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instRing instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instValuedWithZeroMultiplicativeInt	—	IsTopologicalDivisionRing.toIsTopologicalRing Valued.isTopologicalDivisionRing Valued.toIsUniformAddGroup instIsDomain Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing AbstractCompletion.isDenseInducing valuation_LaurentSeries_equal_extension AbstractCompletion.compare_comp_eq_compare T4Space.t3Space T5Space.toT4Space WithZeroTopology.t5Space Valued.continuous_valuation tendsto_valuation
valuation_def 📖	mathematical	—	Valued.v LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid instValuedWithZeroMultiplicativeInt IsDedekindDomain.HeightOneSpectrum.valuation PowerSeries PowerSeries.instCommRing IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain DivisionRing.toRing Field.toDivisionRing instIsDomain Field.toSemifield IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing HahnSeries.instField instAlgebraPowerSeries Semifield.toCommSemiring instIsFractionRingPowerSeries PowerSeries.idealX	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
valuation_le_iff_coeff_lt_eq_zero 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt WithZero.exp HahnSeries.coeff	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing coeff_zero_of_lt_valuation single_order_mul_powerSeriesPart map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass valuation_single_zpow neg_neg mul_comm le_mul_inv_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono Multiplicative.isOrderedCancelMonoid WithZero.exp_neg mul_inv WithZero.exp_add le_trans IsPrincipalIdealRing.isDedekindDomain PowerSeries.instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing instIsFractionRingPowerSeries IsDedekindDomain.HeightOneSpectrum.valuation_le_one WithZero.log_le_iff_le_exp one_ne_zero NeZero.one WithZero.instNontrivial le_neg Int.instAddLeftMono covariant_swap_add_of_covariant_add WithZero.log_one neg_zero LT.lt.le intValuation_le_iff_coeff_lt_eq_zero powerSeriesPart_coeff neg_nonpos_of_nonneg sub_eq_neg_add neg_sub
valuation_le_iff_coeff_lt_log_eq_zero 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt HahnSeries.coeff	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing WithZero.exp.eq_1 neg_neg valuation_le_iff_coeff_lt_eq_zero WithZero.log_exp
valuation_single_zpow 📖	mathematical	—	DFunLike.coe Valuation HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid HahnSeries.instRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt ZeroHom HahnSeries.instZero ZeroHom.funLike HahnSeries.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing WithZero.exp	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.ofPowerSeries_X_pow PowerSeries.coe_pow valuation_X_pow map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass HahnSeries.inv_single neg_neg inv_one WithZero.exp_neg

LaurentSeries.Cauchy

Definitions

Name	Category	Theorems
coeff 📖	CompOp	3 math math: coeff_tendsto, coeff_support_bddBelow, exists_lb_support
limit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_eventually_equal 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	Filter.Eventually	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid exists_lb_coeff_ne Set.iInter_congr_Prop le_of_lt lt_max_of_lt_right Set.ext Filter.eventually_iff Filter.biInter_mem Set.finite_Icc coeff_tendsto Filter.principal_singleton Filter.sets_of_superset HasSubset.Subset.trans Set.instIsTransSubset
coeff_support_bddBelow 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	BddBelow Function.support coeff	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid exists_lb_support not_le
coeff_tendsto 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	Filter.Tendsto HahnSeries.coeff Filter.principal Set Set.instSingletonSet coeff	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid le_of_eq DiscreteUniformity.inst Cauchy.map LaurentSeries.uniformContinuous_coeff Filter.principal_singleton DiscreteUniformity.eq_pure_cauchyConst
eventually_mem_nhds 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace limit	Filter.Eventually Set.instMembership	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid Valued.mem_nhds WithZero.lt_log_iff_exp_lt WithZero.instNontrivial neg_sub IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono Int.instZeroLEOneClass Filter.Eventually.mono coeff_eventually_equal lt_of_le_of_lt LaurentSeries.valuation_le_iff_coeff_lt_eq_zero HahnSeries.coeff_sub sub_eq_zero
exists_lb_coeff_ne 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	Filter.Eventually	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid exists_lb_eventual_support exists_lb_support Filter.sets_of_superset lt_of_lt_of_le min_le_left min_le_right
exists_lb_eventual_support 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	Filter.Eventually	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid WithZero.coe_ne_zero Filter.mem_prod_iff Filter.le_def Filter.HasBasis.mem_of_mem Valued.hasBasis_uniformity Filter.forall_mem_nonempty_iff_neBot Filter.inter_mem_iff LaurentSeries.valuation_le_iff_coeff_lt_eq_zero sub_zero Set.IsPWO.isWF HahnSeries.isPWO_support' HahnSeries.support_nonempty_iff LaurentSeries.eq_coeff_of_valuation_sub_lt lt_of_lt_of_le le_of_lt min_le_right Function.notMem_support Set.IsWF.not_lt_min lt_trans min_le_left Filter.mem_of_superset Filter.inter_mem
exists_lb_support 📖	mathematical	Cauchy LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valued.toUniformSpace HahnSeries.instRing Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid LaurentSeries.instValuedWithZeroMultiplicativeInt	coeff	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid exists_lb_eventual_support Ultrafilter.eq_of_le_pure Cauchy.map LaurentSeries.uniformContinuous_coeff coeff_tendsto Filter.principal_singleton Filter.mem_of_superset

PowerSeries

Definitions

Name	Category	Theorems
idealX 📖	CompOp	5 math math: intValuation_eq_of_coe, LaurentSeries.exists_Polynomial_intValuation_lt, RatFunc.valuation_eq_LaurentSeries_valuation, intValuation_X, LaurentSeries.valuation_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_C 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing C Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid HahnSeries.C	—	HahnSeries.ofPowerSeries_C Int.instIsStrictOrderedRing
coe_X 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing X ZeroHom HahnSeries.instZero ZeroHom.funLike HahnSeries.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	HahnSeries.ofPowerSeries_X Int.instIsStrictOrderedRing
coe_add 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib HahnSeries.instAdd AddCommMonoid.toAddMonoid	—	RingHom.map_add IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_mul 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing MvPowerSeries.instMul HahnSeries.instMul Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid	—	RingHom.map_mul IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_neg 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup HahnSeries.instNeg	—	RingHom.map_neg IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_one 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing MvPowerSeries.instOne HahnSeries.instOne NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHom.map_one IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_pow 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid	—	RingHom.map_pow IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_smul 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instAddCommMonoid instModule HahnSeries.instSMul IsStrictOrderedRing.toIsOrderedCancelAddMonoid	—	HahnSeries.ext Int.instIsStrictOrderedRing IsStrictOrderedRing.toIsOrderedCancelAddMonoid coeff_coe smul_ite smul_zero
coe_sub 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid instAddGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne HahnSeries.instSub	—	RingHom.map_sub IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coe_zero 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing instZero HahnSeries.instZero	—	RingHom.map_zero IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
coeff_coe 📖	mathematical	—	HahnSeries.coeff SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom PowerSeries HahnSeries instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing LinearMap RingHom.id instAddCommMonoid instModule Semiring.toModule LinearMap.instFunLike coeff	—	Int.instIsStrictOrderedRing LaurentSeries.coeff_coe_powerSeries LE.le.not_gt StrictMono.injective Nat.strictMono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero Nat.instIsOrderedCancelAddMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid HahnSeries.ofPowerSeries_apply HahnSeries.embDomain_notin_image_support Set.image_congr
intValuation_X 📖	mathematical	—	DFunLike.coe Valuation PowerSeries WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing instCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.intValuation IsPrincipalIdealRing.isDedekindDomain instIsDomain DivisionRing.toRing Field.toDivisionRing instIsDomain Field.toSemifield IsDiscreteValuationRing.toIsPrincipalIdealRing instIsDiscreteValuationRing idealX X DivisionSemiring.toSemiring Semifield.toDivisionSemiring WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain instIsDomain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing instIsDiscreteValuationRing Polynomial.coe_X Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain intValuation_eq_of_coe IsDedekindDomain.HeightOneSpectrum.intValuation_singleton Polynomial.X_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.idealX_span
intValuation_eq_of_coe 📖	mathematical	—	DFunLike.coe Valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing CommRing.toRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.intValuation IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instIsDomain EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain Polynomial.idealX PowerSeries instCommRing instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing instIsDiscreteValuationRing idealX Polynomial.toPowerSeries	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain EuclideanDomain.to_principal_ideal_domain instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing instIsDiscreteValuationRing Valuation.map_zero Polynomial.coe_zero Ideal.uniqueFactorizationMonoid IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg Int.instCharZero IsLocalRing.toNontrivial Field.instIsLocalRing IsDedekindDomain.HeightOneSpectrum.ne_bot count_associates_factors_eq Ideal.span_singleton_prime Polynomial.X_ne_zero Polynomial.prime_X ValuationRing.toPreValuationRing of_isDiscreteValuationRing Field.isDomain IsDedekindDomain.HeightOneSpectrum.isPrime IsDomain.to_noZeroDivisors PrincipalIdealRing.to_uniqueFactorizationMonoid instUniqueFactorizationMonoid count_span_normalizedFactors_eq_of_normUnit Polynomial.normUnit_X normUnit_X X_prime normalized_count_X_eq_of_coe

RatFunc

Definitions

Name	Category	Theorems
coeToLaurentSeries 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply_div 📖	mathematical	—	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield instField instIsDomain HahnSeries.instSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap liftAlgebra HahnSeries.instField Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id instFaithfulSMulPolynomialLaurentSeries instDiv instAlgebraOfPolynomial DivInvMonoid.toDiv HahnSeries.instDivInvMonoid	—	instIsDomain IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsOrderedAddMonoid instFaithfulSMulPolynomialLaurentSeries map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.algebraMap_apply isScalarTower_liftAlgebra
coe_X 📖	mathematical	—	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield instField HahnSeries.instSemiring Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap liftAlgebra HahnSeries.instField Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid HahnSeries.powerSeriesAlgebra Int.instSemiring Int.instIsStrictOrderedRing Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id instFaithfulSMulPolynomialLaurentSeries X instIsDomain ZeroHom HahnSeries HahnSeries.instZero ZeroHom.funLike HahnSeries.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	Int.instIsOrderedAddMonoid Int.instIsStrictOrderedRing instFaithfulSMulPolynomialLaurentSeries instIsDomain IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsScalarTower.algebraMap_apply isScalarTower_liftAlgebra Polynomial.coe_X HahnSeries.ofPowerSeries_X
coe_coe 📖	mathematical	—	DFunLike.coe RingHom PowerSeries HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield PowerSeries.instSemiring HahnSeries.instNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Int.instSemiring RingHom.instFunLike HahnSeries.ofPowerSeries Int.instIsStrictOrderedRing Polynomial.toPowerSeries RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LaurentSeries NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommSemiring.toSemiring Semifield.toCommSemiring instField HahnSeries.instSemiring Int.instAddCommMonoid algebraMap liftAlgebra HahnSeries.instField Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid HahnSeries.powerSeriesAlgebra Polynomial CommRing.toCommSemiring Polynomial.commSemiring PowerSeries.algebraPolynomial Algebra.id instFaithfulSMulPolynomialLaurentSeries coePolynomial instIsDomain	—	Int.instIsStrictOrderedRing Int.instIsOrderedAddMonoid instFaithfulSMulPolynomialLaurentSeries instIsDomain IsStrictOrderedRing.toIsOrderedCancelAddMonoid isScalarTower_liftAlgebra
instFaithfulSMulPolynomialLaurentSeries 📖	mathematical	—	FaithfulSMul Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toSMul Polynomial.commSemiring Semifield.toCommSemiring HahnSeries.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Int.instSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing CommSemiring.toSemiring HahnSeries.powerSeriesAlgebra PowerSeries.algebraPolynomial Algebra.id	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing faithfulSMul_iff_algebraMap_injective Polynomial.algebraMap_hahnSeries_injective
single_inv 📖	mathematical	—	DFunLike.coe ZeroHom HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain HahnSeries.instZero ZeroHom.funLike HahnSeries.single InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield HahnSeries.instField Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid	—	eq_inv_of_mul_eq_one_right Int.instIsOrderedAddMonoid HahnSeries.single_mul_single add_neg_cancel mul_inv_cancel₀
single_one_eq_pow 📖	mathematical	—	DFunLike.coe ZeroHom HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring HahnSeries.instZero ZeroHom.funLike HahnSeries.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero HahnSeries.instSemiring Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing	—	IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing HahnSeries.single_pow mul_one one_pow
single_zpow 📖	mathematical	—	DFunLike.coe ZeroHom HahnSeries SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain HahnSeries.instZero ZeroHom.funLike HahnSeries.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toZPow HahnSeries.instDivInvMonoid Int.instAddCommGroup Int.instLinearOrder Int.instIsOrderedAddMonoid	—	Int.instIsOrderedAddMonoid single_one_eq_pow Nat.cast_one inv_one HahnSeries.inv_single zpow_neg zpow_natCast IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing
valuation_eq_LaurentSeries_valuation 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.commRing IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id instIsFractionRingPolynomial Polynomial.idealX LaurentSeries MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HahnSeries.instField Int.instAddCommGroup Int.instIsOrderedAddMonoid PowerSeries PowerSeries.instCommRing PowerSeries.instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing LaurentSeries.instAlgebraPowerSeries Semifield.toCommSemiring LaurentSeries.instIsFractionRingPowerSeries PowerSeries.idealX RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring HahnSeries.instSemiring instLatticeInt RingHom.instFunLike algebraMap liftAlgebra HahnSeries.powerSeriesAlgebra Polynomial.commSemiring PowerSeries.algebraPolynomial instFaithfulSMulPolynomialLaurentSeries	—	induction_on' instIsDomain Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain instIsFractionRingPolynomial Int.instIsOrderedAddMonoid PowerSeries.instIsDomain IsDiscreteValuationRing.toIsPrincipalIdealRing PowerSeries.instIsDiscreteValuationRing LaurentSeries.instIsFractionRingPowerSeries instFaithfulSMulPolynomialLaurentSeries mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial mk_eq_mk' PowerSeries.instNoZeroDivisors PowerSeries.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsFractionRing.mk'_eq_div map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.algebraMap_apply isScalarTower_liftAlgebra PowerSeries.intValuation_eq_of_coe IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'

(root)

Definitions

Name	Category	Theorems
LaurentSeries 📖	CompOp	48 math math: RatFunc.instFaithfulSMulPolynomialLaurentSeries, LaurentSeries.LaurentSeriesRingEquiv_def, LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, LaurentSeries.ofPowerSeries_powerSeriesPart, RatFunc.coe_X, LaurentSeries.coe_algebraMap, RatFunc.coe_coe, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, LaurentSeries.val_le_one_iff_eq_coe, LaurentSeries.algebraMap_apply, LaurentSeries.derivative_iterate_coeff, LaurentSeries.exists_ratFunc_val_lt, LaurentSeries.derivative_apply, LaurentSeries.of_powerSeries_localization, RatFunc.valuation_eq_LaurentSeries_valuation, LaurentSeries.coe_X_compare, LaurentSeries.hasseDeriv_comp_coeff, RatFunc.algebraMap_apply_div, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.hasseDeriv_coeff, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, LaurentSeries.valuation_LaurentSeries_equal_extension, LaurentSeries.hasseDeriv_single_add, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, LaurentSeries.hasseDeriv_comp, LaurentSeries.powerSeriesRingEquiv_coe_apply, LaurentSeries.powerSeriesEquivSubring_apply, LaurentSeries.powerSeriesEquivSubring_coe_apply, LaurentSeries.instLaurentSeriesComplete, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.valuation_compare, LaurentSeries.coe_range_dense, LaurentSeries.comparePkg_eq_extension, LaurentSeries.valuation_def, LaurentSeries.derivative_iterate, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, LaurentSeries.uniformContinuous_coeff, LaurentSeries.hasseDeriv_zero, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries, LaurentSeries.instIsFractionRingPowerSeries, LaurentSeries.powerSeriesPart_zero, LaurentSeries.exists_ratFunc_eq_v, LaurentSeries.hasseDeriv_single, LaurentSeries.powerSeriesPart_eq_zero

---

← Back to Index