## 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


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


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: May 11 2021 at 16:22 UTC