Commit 2022-12-10 07:00 f178c0e2

View on Github →

refactor(topology/instances/add_circle): redefine equiv_add_circle (#17881) Use quotient_add_group.congr. Also define add_aut.mul_left and add_aut.mul_right.

Estimated changes

Created src/algebra/ring/add_aut.lean

added def add_aut.mul_left

added def add_aut.mul_right

added theorem add_aut.mul_right_apply

added theorem add_aut.mul_right_symm_apply

Modified src/group_theory/subgroup/basic.lean

added theorem monoid_hom.map_zpowers

Modified src/topology/instances/add_circle.lean