complete — Mathlib

English

The norm of p−1 as a p-adic integer is 1.

Русский

Норма числа p−1 в p-адической системе равна 1.

LaTeX

$$$\\|((p-1))\\|_p = 1$$$

Lean4

instance complete : CauSeq.IsComplete ℚ_[p] norm where
  isComplete
    f :=
    by
    have cau_seq_norm_e : IsCauSeq padicNormE f := fun ε hε =>
      by
      have h := isCauSeq f ε (mod_cast hε)
      dsimp [norm] at h
      exact mod_cast h
    obtain ⟨q, hq⟩ := Padic.complete'' ⟨f, cau_seq_norm_e⟩
    exists q
    intro ε hε
    obtain ⟨ε', hε'⟩ := exists_rat_btwn hε
    norm_cast at hε'
    obtain ⟨N, hN⟩ := hq ε' hε'.1
    exists N
    intro i hi
    have h := hN i hi
    change norm (f i - q) < ε
    refine lt_trans ?_ hε'.2
    dsimp [norm]
    exact mod_cast h

Похожие утверждения