Theorems · Theorem · commutative algebra
LaurentSeries.powerSeriesRingEquiv_coe_apply
∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
↑((LaurentSeries.powerSeriesRingEquiv K) f) =
(LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f)- Defined in
- Mathlib.RingTheory.LaurentSeries
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 187 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.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHomstatement · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement · cited by 5,681
- RingEquivstatement · cited by 1,147
- PowerSeriesstatement and proof · cited by 797
- HahnSeriesstatement · cited by 528
- RatFuncstatement · cited by 301
- ValuationSubringstatement · cited by 187
- IsDedekindDomain.HeightOneSpectrum.adicCompletionstatement · cited by 93
- LaurentSeriesstatement · cited by 64
- HahnSeries.ofPowerSeriesstatement · cited by 45
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.