mathlib3
f8355031
- feat(topology/instances/ennreal): curried version of `ennreal.tsum_prod` (#18124)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(topology/instances/ennreal): curried version of `ennreal.tsum_prod` (#18124) Add a version of `ennreal.tsum_prod` for functions `f : α × β → ℝ≥0∞` rather than `f : α → β → ℝ≥0∞`.
Author
dtumad
Parents
36a35211
Loading