mathlib3
0490b432 - refactor(geometry/manifold/instances/circle): split out (topological) group facts (#7951)

Commit
4 years ago
refactor(geometry/manifold/instances/circle): split out (topological) group facts (#7951) Move the group and topological group facts about the unit circle in `ℂ` from `geometry.manifold.instances.circle` to a new file `analysis.complex.circle`. Delete `geometry.manifold.instances.circle`, moving the remaining material to a section in `geometry.manifold.instances.sphere`.
Author
Parents
Loading