Zulip Chat Archive

Stream: maths

Topic: ZMOD


view this post on Zulip Guy Leroy (Aug 01 2018 at 10:54):

Would anyone know what would be a short way to prove 449 ≡ -1 [ZMOD 5]?

view this post on Zulip Kenny Lau (Aug 01 2018 at 10:55):

theorem test : 449  -1 [ZMOD 5] := dec_trivial

view this post on Zulip Kenny Lau (Aug 01 2018 at 10:56):

4.9 seconds

view this post on Zulip Mario Carneiro (Aug 01 2018 at 10:56):

dec_trivial might work, but if it takes too long you can rewrite it to equality of 449 % 5 = (-1) % 5 and prove by norm_num

view this post on Zulip Guy Leroy (Aug 01 2018 at 10:56):

It doesn't work for me, probably because I didn't reimport mathlib recently

view this post on Zulip Guy Leroy (Aug 01 2018 at 10:57):

Ok thanks I 'll try that

view this post on Zulip Kenny Lau (Aug 01 2018 at 10:57):

it isn't like you don't need mathlib to normnum

view this post on Zulip Guy Leroy (Aug 01 2018 at 10:57):

I meant for dec_trivial

view this post on Zulip Mario Carneiro (Aug 01 2018 at 10:57):

I don't think zmod decidability has changed recently

view this post on Zulip Kenny Lau (Aug 01 2018 at 10:57):

theorem test : 449  -1 [ZMOD 5] :=
by unfold int.modeq; norm_num

view this post on Zulip Kenny Lau (Aug 01 2018 at 10:57):

181 ms

view this post on Zulip Guy Leroy (Aug 01 2018 at 10:58):

That works, thanks guys

view this post on Zulip Mario Carneiro (Aug 01 2018 at 10:58):

I think you can even write by norm_num [int.modeq]

view this post on Zulip Guy Leroy (Aug 01 2018 at 11:01):

Yes indeed, even more concise


Last updated: May 11 2021 at 16:22 UTC