Zulip Chat Archive

Stream: new members

Topic: Automorphism


view this post on Zulip Debendro Mookerjee (Mar 25 2020 at 15:09):

How do you define an automorphism in lean?

view this post on Zulip Johan Commelin (Mar 25 2020 at 15:24):

There is equiv. But really, it depends on what you want

view this post on Zulip Johan Commelin (Mar 25 2020 at 15:24):

Do you want to use categories or not?

view this post on Zulip Johan Commelin (Mar 25 2020 at 15:24):

Automorphism of a group? A ring? Something else?

view this post on Zulip Debendro Mookerjee (Mar 25 2020 at 15:26):

ring

view this post on Zulip Johan Commelin (Mar 25 2020 at 15:27):

In that case, I think R \equiv+* R is the thing you want.

view this post on Zulip Johan Commelin (Mar 25 2020 at 15:27):

In other words, equivalences that preserve +, *, 0, and 1.

view this post on Zulip Yury G. Kudryashov (Mar 25 2020 at 16:33):

There is a ring_aut group in data/equiv/ring.


Last updated: May 08 2021 at 04:14 UTC