Theorems · Definition · number theory

Padic.withValRingEquiv

{p : ℕ} → [inst : Fact (Nat.Prime p)] → (Rat.padicValuation p).Completion ≃+* ℚ_[p]

The p-adic numbers are isomorphic as a field to the completion of the rationals at the p-adic valuation.

Defined in

Mathlib.NumberTheory.Padics.WithVal

Cited by

3 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact