Theorems · Definition · commutative algebra
LaurentSeries.RatFuncAdicCompl
(K : Type u_2) → [Field K] → Type u_2
An abbreviation for the X-adic completion of K⟮X⟯
- Defined in
- Mathlib.RingTheory.LaurentSeries
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 127 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- RatFuncproof · cited by 301
- IsDedekindDomain.HeightOneSpectrum.adicCompletionproof · cited by 93
- Polynomial.idealXproof · cited by 23
Cited by15
Results whose statement or proof uses this declaration.
- LaurentSeries.LaurentSeriesRingEquivstatement · cited by 8
- LaurentSeries.ratfuncAdicComplRingEquivstatement and proof · cited by 3
- LaurentSeries.valuation_comparestatement · cited by 3
- LaurentSeries.mem_integers_of_powerSeriesstatement · cited by 1
- LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubringstatement · cited by 1
- LaurentSeries.ratfuncAdicComplRingEquiv_applystatement and proof · cited by 1
- LaurentSeries.comparePkgstatement · cited by 1
- LaurentSeries.exists_powerSeries_of_memIntegersstatement and proof · cited by 1
- LaurentSeries.LaurentSeriesAlgEquivstatement · cited by 0
- LaurentSeries.powerSeriesRingEquiv_coe_applystatement · cited by 0
- LaurentSeries.LaurentSeriesRingEquiv_defstatement · cited by 0
- LaurentSeries.powerSeries_ext_subringstatement and proof · cited by 0