bases): define `filter.has_basis`
#1896

Merged

feat(order/filter/bases): define `filter.has_basis` #1896

mergify merged 10 commits into master from bases

feat(*): assorted simple lemmas, simplify some proofs

f7e9d1dd

feat(order/filter/bases): define `filter.has_basis`

c6906f5b

Add `@[nolint]`

21afff21

+1 lemma, +1 simplified proof

9f910574

urkud added blocked-by-other-PR

Merge branch 'assorted-lemmas' into bases

c3c692a0

jcommelin assigned

PatrickMassot 6 years ago

Merge branch 'master' into bases

a83da480

urkud removed blocked-by-other-PR

Merge branch 'master' into bases

4fe08a52

sgouezel commented on 2020-01-21

Remove whitespaces

626dfb4e

urkud commented on 2020-01-21

Ref. note nolint_ge

9553790f

sgouezel approved these changes on 2020-01-22

sgouezel added ready-to-merge

Merge branch 'master' into bases

7d3e0343

mergify merged 69099f00 into master 6 years ago

mergify deleted the bases branch 6 years ago

Reviewers

sgouezel

Assignees

PatrickMassot

Labels

ready-to-merge

Milestone

No milestone