add_circle): redefine `equiv_add_circle` (#17881)

Commit

3 years ago

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`.

Author

urkud

Parents

f1d5b468

mathlib3 f178c0e2 - refactor(topology/instances/add_circle): redefine `equiv_add_circle` (#17881)

mathlib3
f178c0e2 - refactor(topology/instances/add_circle): redefine `equiv_add_circle` (#17881)