not_int_of_not_padic_int — Mathlib

English

If a rational is not a p-adic integer, it is not an integer.

Русский

Если рациональное число не является p-пadic целым, то оно не является целым числом.

LaTeX

$$$ \forall p,\ 1 < padicNorm p a \rightarrow a \notin \mathbb{Z} $$$

Lean4

/-- If a rational is not a p-adic integer, it is not an integer. -/
theorem not_int_of_not_padic_int (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)] (H : 1 < padicNorm p a) : ¬a.isInt :=
  by
  contrapose! H
  rw [Rat.eq_num_of_isInt H]
  apply padicNorm.of_int

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