Ring automorphisms #
Implementation notes #
The definition of multiplication in the automorphism group agrees with function composition,
equiv.perm, and multiplication in
category_theory.End, but not with
This file is kept separate from
data/equiv/ring so that
group_theory.perm is free to use
equivalences (and other files that use them) before the group structure is defined.
The group operation on automorphisms of a ring is defined by
λ g h, ring_equiv.trans h g.
This means that multiplication agrees with composition,
(g*h)(x) = g (h x).