mathlib3
577e3a22
- chore(topology/algebra/uniform_group): Remove newline after docstring (#11671)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(topology/algebra/uniform_group): Remove newline after docstring (#11671) Yael pointed out that #11662 added an erroneous newline after a docstring. This PR removes that newline.
Author
tb65536
Parents
946454a8
Loading