Module

CompactDenominator.lean

Nyll.ValuedFieldTheory.LocalField.Padic.CompactDenominator

1 declaration indexed from sourceView source ↗

Module documentation

A common denominator for a compact family of p-adic numbers

A continuous family on a compact space can be multiplied by one power of p so that every value lies in the actual p-adic integer ring.

Imports2

Mathlib.NumberTheory.Padics.PadicIntegers
Mathlib.Topology.Order.Compact

Imported by2

theorem

exists_pow_mul_norm_le_one

L22 ↗

LocalFieldTheory.exists_pow_mul_norm_le_one

Documentation

A compact continuous family of p-adic numbers has a uniform integral denominator.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem exists_pow_mul_norm_le_one {Y : Type*} [TopologicalSpace Y] [CompactSpace Y]
    (f : Y → ℚ_[p]) (hf : Continuous f) :
    ∃ n : ℕ, ∀ y : Y, ‖(p : ℚ_[p]) ^ n * f y‖ ≤ 1

Module documentation

A common denominator for a compact family of p-adic numbers

Declarations

exists_pow_mul_norm_le_one