Zulip Chat Archive

Stream: maths

Topic: integral rational numbers


Johan Commelin (Jun 03 2019 at 07:47):

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 (Jun 03 2019 at 07:48):

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

Reid Barton (Jun 03 2019 at 08:45):

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

Reid Barton (Jun 03 2019 at 08:46):

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

Johan Commelin (Jun 03 2019 at 08:51):

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

Kevin Buzzard (Jun 03 2019 at 08:52):

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 (Jun 03 2019 at 08:52):

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

Kevin Buzzard (Jun 03 2019 at 08:52):

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

Johan Commelin (Jun 03 2019 at 08:54):

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 (Jun 03 2019 at 08:55):

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 (Jun 03 2019 at 08:56):

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 (Jun 03 2019 at 08:57):

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


Last updated: Dec 20 2023 at 11:08 UTC