Stream: new members
Ashvni Narayanan (Jun 24 2020 at 17:23):
This is a general question. Suppose I have some space K, and a function from K to \Z. For elements a,b,c in K, I have the relation h : ab = c. I want to show that f(ab) = f(c). How can I show this? I tried rw h, but I get the error
rewrite tactic failed, did not find instance of the pattern in the target expression a * b
Any help is appreciated. Thank you!
Bhavik Mehta (Jun 24 2020 at 17:24):
Ashvni Narayanan (Jun 24 2020 at 17:31):
Ah, the congr tactic works, but the problem seems to be elsewhere. Thank you!
Last updated: May 10 2021 at 00:31 UTC