WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — P-adic number

Revision #2291 → #2960 · back to history

modifiedQ_p as fraction field of completion of localization of Z at (p)0b738d7e93da
FieldFrom #2291To #2960
note`Padic.adicCompletionEquiv` identifies ℚ_[p] with the (p)-adic completion of ℚ; together with `PadicInt.adicCompletionIntegersEquiv` this exactly formalizes 'ℚ_[p] = Frac(completion of ℤ_(p))'.`Padic.adicCompletionEquiv` identifies ℚ_[p] with the (p)-adic completion of ℤ; together with `PadicInt.adicCompletionIntegersEquiv` this exactly formalizes 'ℚ_[p] = Frac(completion of ℤ_(p))'.