## Stream: new members

### Topic: tactic for doing calculation with mod

#### Patrick Lutz (Jun 21 2020 at 21:43):

Is there a tactic (or some other way I guess) to take care of calculations in modular arithmetic? E.g. something that would easily prove the following

import data.nat.basic

example (a b c : ℕ) (ha : a % 5 = 1) (hb : b % 5 = 3)
(hc : c % 5 = 4) : (a^2 + (b + 2*c)^3) % 5 = 2 := sorry


Right now I can prove this with a series of rewrites and then a call to ring, but it seems too involved. Is there a better way?

#### Chris Hughes (Jun 21 2020 at 21:47):

I would avoid the use of % and use the type zmod for most things like this.

#### Jalex Stark (Jun 21 2020 at 21:48):

import tactic

import data.nat.basic
import data.zmod.basic

example (a b c : zmod 5) (ha : a = 1) (hb : b = 3)
(hc : c = 4) : (a^2 + (b + 2*c)^3) = 2 :=
begin
rw [ha, hb, hc], ring,
end


Last updated: May 11 2021 at 12:15 UTC