circle): The circle group is commutative (#11368)

Commit

4 years ago

refactor(analysis/complex/circle): The circle group is commutative (#11368) This PR upgrades the `group circle` instance to a `comm_group circle` instance.

Author

tb65536

Parents

e8839a30

mathlib3 de9944b1 - refactor(analysis/complex/circle): The circle group is commutative (#11368)

mathlib3
de9944b1 - refactor(analysis/complex/circle): The circle group is commutative (#11368)