What's the lean4 code of this simple problem?I am a newbie.

Stream: new members

[wan loeng]

example.png

[wan loeng]

I am a student who is just starting to learn lean.Could someone help me?

[Rémy Degenne]

Did you attempt to write the statement in Lean? Can you be more precise about what you did not manage to do? Is that your homework?
If you want to get useful help you should show us what you tried and ask more detailed questions.

[Rémy Degenne]

Also this is the wrong channel for such questions. There is a #new members channel that would be more appropriate.

[Notification Bot]

This topic was moved here from #lean4 > What's the lean4 code of this simple problem?I am a newbie. by Kevin Buzzard.

[Kevin Buzzard]

One issue with this question is that this quesiton is open-ended and so cannot really be formalized in its current state. How would you feel if I gave you the following answer: "the elements of $A(S)$ which commute with the given $f$ are $\{g\in A(S)\,|\,g\circ f=f\circ g\}$ "? If that answer is not acceptable to you then this means you haven't asked the right question yet.