norm_intCast_lt_one_iff — Mathlib

English

For k ∈ ℤ, ‖k‖_p < 1 if and only if p divides k.

Русский

Для k ∈ ℤ выполняется: ‖k‖_p < 1 тогда и только тогда, когда p делит k.

LaTeX

$$$‖k‖_p < 1 \\iff p \\mid k$$$

Lean4

@[simp]
theorem norm_intCast_lt_one_iff {k : ℤ} : ‖(k : ℚ_[p])‖ < 1 ↔ ↑p ∣ k :=
  by
  constructor
  · intro h
    contrapose! h
    apply le_of_eq
    rw [eq_comm]
    calc
      ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := (eq_padicNorm _)
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h
  · rintro ⟨x, rfl⟩
    push_cast
    rw [padicNormE.mul]
    calc
      _ ≤ ‖(p : ℚ_[p])‖ * 1 := mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
      _ < 1 := by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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