mathlib3
1d4dbd08
- feat(analysis/specific_limits/basic)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
feat(analysis/specific_limits/basic) Added a lemma for the limit of `1/n` into an `ℝ` algebra.
Author
xgenereux
Parents
fff4a338
Loading