mathlib3
cf5aea0a
- chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512) Also make the argument explicit
Author
eric-wieser
Parents
094b1f51
Loading