Stream: Beginner Questions

Topic: substituting into a congruence

view this post on Zulip Jakub Kądziołka (Feb 07 2021 at 11:58):

is there a tactic or simproc that will use [a = b] (mod n) to rewrite, say, [a^k * (a + c) = a^a] (mod n) into [b^k * (b + c) = b^a] (mod n)? I'm getting just about annoyed enough to try writing one myself, but I'd rather avoid it if it already exists somewhere.

view this post on Zulip Manuel Eberl (Feb 07 2021 at 13:29):

Rewriting w.r.t. relations other than equality is one of those things that would be nice to have. I think we had a couple of students working on this sort of thing but somehow we never got something finished out of it (I think?).

Personally, I usually just do chains of [_ = _] (mod _) using also just like I would do with regular equations and show each step using cong_add, cong_diff, etc.

Last updated: Aug 13 2022 at 05:18 UTC