norm_sub_modPart — Mathlib

English

If ⎯ ≤ 1 then the p-adic norm of ⟨r⟩ − modPart(p,r) in ℤ_p is less than 1.

Русский

Если норма ⎯ ≤ 1, то норма в ℤ_p разности ⟨r⟩ и modPart(p,r) меньше 1.

LaTeX

$$$\\\\|\\\\langle r,h\\\\rangle - \\mathrm{modPart}(p,r)\\\\|_p < 1$$$

Lean4

theorem norm_sub_modPart (h : ‖(r : ℚ_[p])‖ ≤ 1) : ‖(⟨r, h⟩ - modPart p r : ℤ_[p])‖ < 1 :=
  by
  let n := modPart p r
  rw [norm_lt_one_iff_dvd, ← (isUnit_den r h).dvd_mul_right]
  suffices ↑p ∣ r.num - n * r.den by
    convert (map_dvd (Int.castRingHom ℤ_[p])) this
    simp only [n, sub_mul, Int.cast_natCast, eq_intCast, Int.cast_mul, sub_left_inj, Int.cast_sub]
    apply Subtype.coe_injective
    simp only [coe_mul, coe_natCast]
    norm_cast
    simp
  exact norm_sub_modPart_aux r h

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