Zulip Chat Archive

Stream: new members

Topic: Function


view this post on Zulip 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!

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 17:24):

rw h should work here - can you post a #mwe? If you really, really can't get it to work, two things you could try are tactic#conv or tactic#congr

view this post on Zulip 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