ModuleNonarchimedeanLocalField.lean
Nyll.ValuedFieldTheory.LocalField.Padic.NonarchimedeanLocalField
5 declarations indexed from sourceView source ↗ Module documentation
The p-adic field as a nonarchimedean local field
This file connects Mathlib's normed and valuative structures on ℚ_p to the topology-first local-field interface used by this library.
Declarations
LocalFieldTheory.Padic.mulValuation_le_one_iff_norm_le_one
DocumentationThe canonical multiplicative valuation of ℚ_p is at most one exactly when the p-adic norm is at most one.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped ValuativeRel WithZero
namespace LocalFieldTheory.Padic
variable (p : ℕ) [Fact p.Prime]
LocalFieldTheory.Padic.integer_mem_iff_norm_le_one
DocumentationThe integer ring defined by the canonical valuative relation on ℚ_p consists exactly of the elements of norm at most one.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped ValuativeRel WithZero
namespace LocalFieldTheory.Padic
variable (p : ℕ) [Fact p.Prime]
LocalFieldTheory.Padic.normedFieldValuation_compatible_padic
DocumentationThe norm-induced valuation on ℚ_p is compatible with the canonical p-adic valuation ordering.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped ValuativeRel WithZero
namespace LocalFieldTheory.Padic
variable (p : ℕ) [Fact p.Prime]
LocalFieldTheory.Padic.padicIsValuativeTopology
DocumentationThe usual topology on ℚ_p is induced by its canonical valuation.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped ValuativeRel WithZero
namespace LocalFieldTheory.Padic
variable (p : ℕ) [Fact p.Prime]
LocalFieldTheory.Padic.padicIsNonarchimedeanLocalField
DocumentationMathlib's p-adic field is a nonarchimedean local field for the topology-first interface used by local class field theory.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped ValuativeRel WithZero
namespace LocalFieldTheory.Padic
variable (p : ℕ) [Fact p.Prime]