data.int.gcd

Stream: mathlib4

[Riccardo Brasca]

I am porting data.int.gcd, see #981.

The file uses docs#int.nat_mod. This doesn't exist in mathlib4, right?

I know that mod is going to change in Std, so I am not fixing everything at the moment.

[Riccardo Brasca]

Oh, I just realized that it depends on data.int.order.basic, that is very far from having been ported :(

[Scott Morrison]

data.int.order.basic is now basically ready, it just has one error, so feel free to depend on it

[Kevin Buzzard]

my version has 0 errors ;-) (but it avoids the question which is actually at stake there)

[Kevin Buzzard]

(deleted)

[Scott Morrison]

https://github.com/leanprover-community/mathlib4/pull/980 is almost ready to go, but mysteriously in Mathlib.Tactic.Ring.Basic I had to make Ex[Base|Prod|Sum].evalPos partial. I don't see what change caused this, but I don't see how it could be problematic so I'm not going to wait on this. Just noting in case @Mario Carneiro sees some reason to be concerned.

[Mario Carneiro]

Note that there are already some definitions in there which are partial for performance, see Ex[Base|Prod|Sum].{eq,cmp}

[Mario Carneiro]

what happens if it's not marked as partial?

[Riccardo Brasca]

I am not sure I will have time today, if anyone wants to contribute to the PR please go ahead.