mathlib
420fabf7
- chore(analysis/normed_space/exponential): replace `1/x` with `x⁻¹` (#13971)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(analysis/normed_space/exponential): replace `1/x` with `x⁻¹` (#13971) Note that `one_div` makes `⁻¹` the simp-normal form.
Author
eric-wieser
Parents
03f5ac93
Loading