Zulip Chat Archive
Stream: maths
Topic: ZMOD
Guy Leroy (Aug 01 2018 at 10:54):
Would anyone know what would be a short way to prove 449 ≡ -1 [ZMOD 5]?
Kenny Lau (Aug 01 2018 at 10:55):
theorem test : 449 ≡ -1 [ZMOD 5] := dec_trivial
Kenny Lau (Aug 01 2018 at 10:56):
4.9 seconds
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
Guy Leroy (Aug 01 2018 at 10:56):
It doesn't work for me, probably because I didn't reimport mathlib recently
Guy Leroy (Aug 01 2018 at 10:57):
Ok thanks I 'll try that
Kenny Lau (Aug 01 2018 at 10:57):
it isn't like you don't need mathlib to normnum
Guy Leroy (Aug 01 2018 at 10:57):
I meant for dec_trivial
Mario Carneiro (Aug 01 2018 at 10:57):
I don't think zmod decidability has changed recently
Kenny Lau (Aug 01 2018 at 10:57):
theorem test : 449 ≡ -1 [ZMOD 5] := by unfold int.modeq; norm_num
Kenny Lau (Aug 01 2018 at 10:57):
181 ms
Guy Leroy (Aug 01 2018 at 10:58):
That works, thanks guys
Mario Carneiro (Aug 01 2018 at 10:58):
I think you can even write by norm_num [int.modeq]
Guy Leroy (Aug 01 2018 at 11:01):
Yes indeed, even more concise
Last updated: Dec 20 2023 at 11:08 UTC