mathlib3
41014e50
- rename has_sum and is_sum to summable and has_sum (#912)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
rename has_sum and is_sum to summable and has_sum (#912)
References
#912 - feat(analysis,measure_theory,topology): rename has_sum and is_sum to summable and has_sum
Author
sgouezel
Committer
mergify[bot]
Parents
c4b65da1
Loading