mathlib3
feat(linear_algebra/finite_dimensional): finite dimensional vector spaces
#1241

Merged

feat(linear_algebra/finite_dimensional): finite dimensional vector spaces #1241

mergify merged 10 commits into master from findim

feat(linear_algebra/finite_dimensional): finite dimensional vector sp…

e23c5221

ChrisHughes24 requested a review 6 years ago

jcommelin commented on 2019-07-18

rw `of_span_finite_eq_top` to `of_fg`

3ca6232c

prove infinite.nat_embedding

abb3dfe3

generalize finite_of_linear_independent to noetherian modules

78c79e7c

fix build

c51eba92

Merge branch 'master' into findim

7d338dc0

fix build (ring_theory/polynomial)

b8778542

Merge branch 'findim' of https://github.com/leanprover-community/math…

204635f7

jcommelin commented on 2019-07-22

Merge branch 'master' into findim

ad923072

jcommelin approved these changes on 2019-07-22

jcommelin added ready-to-merge

Merge branch 'master' into findim

fad0e349

mergify merged 3e77fec2 into master 6 years ago

mergify deleted the findim branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone