mathlib3
feat(linear_algebra/dual): add dual vector spaces
#881

Merged

feat(linear_algebra/dual): add dual vector spaces #881

robertylewis merged 4 commits into leanprover-community:master from faabian:dual

feat(linear_algebra/dual): add dual vector spaces

1256b6b0

cipher1024 requested a review from

jcommelin 6 years ago

cipher1024 assigned

robertylewis 6 years ago

jcommelin commented on 2019-04-03

style(linear_algebra/dual): adapt to remarks from PR dsicussion

6a4d5fba

style(linear_algebra/dual): reformat proof of `ker_eq_bot'`

f9cf33c4

digama0 dismissed these changes on 2019-04-08

robertylewis dismissed these changes on 2019-04-08

robertylewis added ready-to-merge

Merge branch 'master' into dual

0fbc32f6

robertylewis requested a review 6 years ago

mergify dismissed their stale review 6 years ago

Pull request has been modified.

mergify dismissed their stale review 6 years ago

Pull request has been modified.

robertylewis approved these changes on 2019-04-08

robertylewis merged 5f1329a2 into master 6 years ago

Reviewers

robertylewis

digama0

jcommelin

Assignees

robertylewis

Labels

ready-to-merge

Milestone

No milestone