Stream: new members
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