In the first part there are theorems of the following form: if α has a group structure and α ≃ β then β has a group structure, and similarly for monoids, semigroups, rings, integral domains, fields and so on.
In the second part there are extensions of equiv called add_equiv, mul_equiv, and ring_equiv, which are datatypes representing isomorphisms of add_monoids/add_groups, monoids/groups and rings. We also introduce the corresponding groups of automorphisms add_aut, mul_aut, and ring_aut.
The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.
The fields for mul_equiv, add_equiv, and ring_equiv now avoid the unbundled is_mul_hom and is_add_hom, as these are deprecated.
Definition of multiplication in the groups of automorphisms agrees with function composition, multiplication in equiv.perm, and multiplication in category_theory.End, not with category_theory.comp.
equiv, mul_equiv, add_equiv, ring_equiv, mul_aut, add_aut, ring_aut
add_equiv α β is the type of an equiv α ≃ β which preserves addition.
mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication.
A multiplicative isomorphism preserves multiplication (canonical form).
A multiplicative isomorphism preserves multiplication (deprecated).
The identity map is a multiplicative isomorphism.
The inverse of an isomorphism is an isomorphism.
Transitivity of multiplication-preserving isomorphisms
e.right_inv in canonical form
e.left_inv in canonical form
a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism)
A multiplicative bijection between two monoids is an isomorphism.
A multiplicative equivalence of groups preserves inversion.
A multiplicative bijection between two monoids is a monoid hom (deprecated -- use to_monoid_hom).
A multiplicative bijection between two groups is a group hom (deprecated -- use to_monoid_hom).
Two multiplicative isomorphisms agree if they are defined by the same underlying function.
Two additive isomorphisms agree if they are defined by the same underlying function.
An additive equivalence of additive groups preserves subtraction.
The group of multiplicative automorphisms.
The group of additive automorphisms.
The group operation on multiplicative automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).
Monoid hom from the group of multiplicative automorphisms to the group of permutations.
The group operation on additive automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).
Monoid hom from the group of multiplicative automorphisms to the group of permutations.
A group is isomorphic to its group of units.
The identity map is a ring isomorphism.
The inverse of a ring isomorphism is a ring isomorphis.
Transitivity of ring_equiv.
A ring isomorphism preserves multiplication.
A ring isomorphism sends one to one.
A ring isomorphism preserves addition.
A ring isomorphism sends zero to zero.
Reinterpret a ring equivalence as a ring homomorphism.
Interpret an equivalence f : α ≃ β as a ring equivalence α ≃+* β.
Interpret an equivalence f : α ≃ β as a ring equivalence α ≃+* β.
Two ring isomorphisms agree if they are defined by the same underlying function.
The group of ring automorphisms.
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) .
Monoid homomorphism from ring automorphisms to additive automorphisms.
Monoid homomorphism from ring automorphisms to multiplicative automorphisms.
Monoid homomorphism from ring automorphisms to permutations.