Zulip Chat Archive
Stream: new members
Topic: Automorphism
Debendro Mookerjee (Mar 25 2020 at 15:09):
How do you define an automorphism in lean?
Johan Commelin (Mar 25 2020 at 15:24):
There is equiv. But really, it depends on what you want
Johan Commelin (Mar 25 2020 at 15:24):
Do you want to use categories or not?
Johan Commelin (Mar 25 2020 at 15:24):
Automorphism of a group? A ring? Something else?
Debendro Mookerjee (Mar 25 2020 at 15:26):
ring
Johan Commelin (Mar 25 2020 at 15:27):
In that case, I think R \equiv+* R is the thing you want.
Johan Commelin (Mar 25 2020 at 15:27):
In other words, equivalences that preserve +, *, 0, and 1.
Yury G. Kudryashov (Mar 25 2020 at 16:33):
There is a ring_aut group in data/equiv/ring.
Last updated: Dec 20 2023 at 11:08 UTC