mathlib3
feat(analysis,measure_theory,topology): rename has_sum and is_sum to summable and has_sum
#912
Merged
Overview
Commits
2
Changes
View On GitHub

feat(analysis,measure_theory,topology): rename has_sum and is_sum to summable and has_sum #912

mergify merged 2 commits into master from summable
sgouezel
sgouezel rename has_sum and is_sum to summable and has_sum
5d3b9f3c
sgouezel sgouezel requested a review 6 years ago
johoelzl
johoelzl approved these changes on 2019-04-10
robertylewis robertylewis changed the title rename has_sum and is_sum to summable and has_sum feat(analysis,measure_theory,topology): rename has_sum and is_sum to summable and has_sum 6 years ago
robertylewis
avigad avigad added ready-to-merge
Merge branch 'master' into 'summable'
33756b6e
mergify mergify merged 41014e50 into master 6 years ago
mergify mergify deleted the summable branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum