padicNorm.not_int_of_not_padic_int and Bool

Stream: mathlib4

[Kevin Buzzard]

The theorem docs#padicNorm.not_int_of_not_padic_int says that if the $p$-adic norm of a : ℚ is greater than one, then ¬a.isInt = true!
My initial guess was that we don't really want Rat.isInt in Mathlib outside tactic code, as it turns out to be Bool-valued, but I've just searched for it and it seems to show up in the following non-tactic code:

In Data.Rat.Defs:

lemma eq_num_of_isInt {q : ℚ} (h : q.isInt) : q = q.num := by ...

in NumberTheory.Padics.PadicNorm as I just mentioned:

/-- 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 ...

and in NumberTheory.Harmonic.Int:

/-- The n-th harmonic number is not an integer for n ≥ 2. -/
theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) : ¬ (harmonic n).isInt := by ...

The only uses of the first two lemmas are in the proof of the third lemma, which isn't used at all.

Do we / should we have a Prop-valued way of saying "this rational number is not an integer"? The reason I'm asking is that I'd like to use the fact that if a rational has p-adic norm > 1 then it's not an integer, but I have my principles and I really don't want to be handling Bools in FLT.

[Ruben Van de Velde]

I think we use \in range coe