mathlib3
doc(linear_algebra/basic): add module and declaration doc strings
#1501

Merged

doc(linear_algebra/basic): add module and declaration doc strings #1501

mergify merged 4 commits into master from linalg

doc(linear_algebra/basic): declaration doc strings

ea9a260c

doc(linear_algebra/basic): improve module doc

226d9b9c

robertylewis requested a review 6 years ago

fpvandoorn commented on 2019-10-02

Update src/linear_algebra/basic.lean

9bbbdca9

fpvandoorn added ready-to-merge

fpvandoorn approved these changes on 2019-10-03

Merge branch 'master' into linalg

dd4d158c

mergify merged 3c58f160 into master 6 years ago

mergify deleted the linalg branch 6 years ago

Reviewers

fpvandoorn

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone