mathlib3
49cf0be5
- refactor(real): protect real.pi (#6039)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
refactor(real): protect real.pi (#6039) Currently, `real.pi` is not protected. This can conflict with `set.pi`. Since it is most often used as `π` through the `real` locale, let's protect it.
Author
sgouezel
Parents
1a7fb7e4
Loading