integral rational numbers

Stream: maths

[Johan Commelin]

I want to write a lemma that says that a rational number is an integer if all its p-adic valuations are nonnegative. What is the correct mathlib-idiomatic way to express this? I currently have

lemma integral_of_padic_val_ge_zero (r : ℚ) (h : ∀ p, nat.prime p → padic_val_rat p r ≥ 0) :
  (r.num : ℚ) = r :=

[Johan Commelin]

The conclusion becomes int.cast r.num = r. Is that a good way, or should we use something else?

[Reid Barton]

There are so many ways one could write this, perhaps it's worth adding a dedicated one is_int

[Reid Barton]

In general it could be defined as being in the image of int.cast

[Johan Commelin]

Yeah... that's part of what I'm after with this question

[Kevin Buzzard]

I have felt for around a year now that for every "troublesome-to-a-mathematician" inclusion (e.g. like int in real) there could be a typeclass on the bigger type (e.g. complex.is_int), or even two typeclasses (the one which stores the int and the one which just says one exists). I have raised this suggestion before. One disadvantage pointed out to me was that now you get a "new int" (in fact several), i.e. {q : rat // is_int q}, which apparently is somehow bad.

[Johan Commelin]

But maybe using r.num instead of some chosen preimage should make things more computable?

[Kevin Buzzard]

One advantage was that you remove all the cast headaches; type class inferences shows is_int z -> is_rat z for example.

[Johan Commelin]

you get a "new int" (in fact several), i.e. {q : rat // is_int q}, which apparently is somehow bad.

Very bad :joy: after all... they aren't equal. Only canonically isomorphic :tears:

[Kevin Buzzard]

Yeah exactly. In some sense that's what makes it bad! You don't want canonically isomorphic stuff, you want stuff which is one of the standard type theory equals :-/

[Kevin Buzzard]

In fact perhaps the reason the CS guys tell us it's bad is precisely because we don't have the transfer tactic which will enable us to port all the stuff we want from one type to the canonically isomorphic one.

[Kevin Buzzard]

[right, as Patrick says, back to mowing the lawn...]