PowerSeries.intValuation_X

∀ {K : Type u_2} [inst : Field K], (PowerSeries.idealX K).intValuation PowerSeries.X = WithZero.exp (-1)

The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤᵐ⁰.

Defined in: Mathlib.RingTheory.LaurentSeries
Cited by: 1 results in Mathlib
Foundations: Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Fieldstatement and proof · cited by 7,404
Polynomial.Xproof · cited by 1,639
Multiplicativestatement and proof · cited by 875
Valuationstatement · cited by 823
PowerSeriesstatement and proof · cited by 797
WithZerostatement and proof · cited by 586
PowerSeries.Xstatement · cited by 183
WithZero.expstatement and proof · cited by 112
IsDedekindDomain.HeightOneSpectrum.intValuationstatement and proof · cited by 53
Polynomial.idealXproof · cited by 23
Polynomial.coe_Xproof · cited by 12

Results whose statement or proof uses this declaration.