mathlib3
feat(*): some simple lemmas about sets and finite sets
#1903

Merged

feat(*): some simple lemmas about sets and finite sets #1903

mergify merged 9 commits into master from set-finset

feat(*): some simple lemmas about sets and finite sets

ed651fd6

urkud added WIP

More lemmas, simplify proofs

be1afa32

urkud removed WIP

urkud added awaiting-review

jcommelin commented on 2020-01-25

urkud removed awaiting-review

urkud added awaiting-author

ChrisHughes24 commented on 2020-01-25

Introduce `finsup.nonempty` and use it.

9f051404

Update src/algebra/big_operators.lean

17c89a80

Revert "Update src/algebra/big_operators.lean"

35a7589b

simp, to_additive

89431ee1

Merge branch 'master' into set-finset

4d8743b0

sgouezel added ready-to-merge

sgouezel removed awaiting-author

sgouezel removed ready-to-merge

sgouezel added awaiting-review

sgouezel commented on 2020-01-25

ChrisHughes24 approved these changes on 2020-01-25

ChrisHughes24 removed awaiting-review

ChrisHughes24 added ready-to-merge

sgouezel commented on 2020-01-25

Add a missing docstring

ad432293

Merge branch 'master' into set-finset

cd0fa53f

mergify merged 9decec2b into master 6 years ago

mergify deleted the set-finset branch 6 years ago

Reviewers

ChrisHughes24

sgouezel

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(*): some simple lemmas about sets and finite sets #1903 Merged

feat(*): some simple lemmas about sets and finite sets #1903

mathlib3
feat(*): some simple lemmas about sets and finite sets
#1903

Merged