PR #779 refactor(*): move matrix.lean to data/ and

refactor(*): move matrix.lean to data/ and #779

ChrisHughes24 merged 1 commit into master from move-matrix-det

refactor(*): move matrix.lean to data/ and determinant.lean to linear…

a191c048

cipher1024 assigned

ChrisHughes24 6 years ago

ChrisHughes24 merged 1f4f2e42 into master 6 years ago

johoelzl deleted the move-matrix-det branch 6 years ago

Reviewers

No reviews

Assignees

ChrisHughes24

Labels

None yet

Milestone

No milestone