mathlib
384c9be2
- feat (analysis/normed_space/basic.lean): implement reverse triangle inequality (#831)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
feat (analysis/normed_space/basic.lean): implement reverse triangle inequality (#831) * implement reverse triangle inequality * make parameters explicit
References
#831 - feat (analysis/normed_space/basic.lean): implement reverse triangle inequality
Author
jdsalchow
Committer
mergify[bot]
Parents
07aa1e3e
Loading