mathlib3
feat(linear_algebra/basis): Dedekind's linear independence of characters
#1595

Merged

feat(linear_algebra/basis): Dedekind's linear independence of characters #1595

mergify merged 6 commits into master from dedekind-indep

feat(linear_algebra/basis): Dedekind's linear independence of characters

5eccc591

kckennylau requested a review from

jcommelin 6 years ago

kckennylau requested a review from

kim-em 6 years ago

feat(linear_algebra/basis): generalize independence of characters to …

d81ad537

ChrisHughes24 commented on 2019-10-23

rwbarton commented on 2019-10-23

rwbarton added awaiting-author

chore(linear_algebra/basis): change proofs

7e2869c7

ChrisHughes24 assigned

ChrisHughes24 6 years ago

rwbarton removed awaiting-author

ChrisHughes24 approved these changes on 2019-10-26

ChrisHughes24 added ready-to-merge

Merge branch 'master' into dedekind-indep

6c8e6d94

commenting the proof

2e95e582

Merge branch 'dedekind-indep' of github.com:leanprover-community/math…

96fbe80f

mergify merged 8eaf478a into master 6 years ago

mergify deleted the dedekind-indep branch 6 years ago

Reviewers

ChrisHughes24

rwbarton

jcommelin

kim-em

Assignees

ChrisHughes24

Labels

ready-to-merge

Milestone

No milestone