Theorems · Theorem · commutative algebra

LaurentSeries.ratfuncAdicComplRingEquiv_apply

∀ (K : Type u_2) [inst : Field K] (x : LaurentSeries.RatFuncAdicCompl K),
  (LaurentSeries.ratfuncAdicComplRingEquiv K) x =
    LaurentSeries.ratfuncAdicComplPkg.compare (LaurentSeries.LaurentSeriesPkg K) x.toCompletion

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

Mathlib docs Source Loogle LeanSearch

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
Fieldstatement and proof · cited by 7,404
Polynomialstatement · cited by 5,681
RingEquivstatement · cited by 1,147
Multiplicativestatement · cited by 875
WithZerostatement · cited by 586
RatFuncstatement · cited by 301
WithValstatement · cited by 151
LaurentSeriesstatement · cited by 64
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletionstatement · cited by 25
Polynomial.idealXstatement · cited by 23
LaurentSeries.RatFuncAdicComplstatement and proof · cited by 11

Cited by1

Results whose statement or proof uses this declaration.

LaurentSeries.coe_X_compareproof · cited by 0