mathlib3
chore(linear_algebra/determinant): simplify det_mul proof
#1392

Merged

chore(linear_algebra/determinant): simplify det_mul proof #1392

mergify merged 3 commits into master from ChrisHughes24-patch-1

chore(linear_algebra/determinant): simplify det_mul proof

2e9c1340

ChrisHughes24 requested a review 6 years ago

make det_mul_aux more readable

9ac0c7c0

sgouezel added ready-to-merge

sgouezel approved these changes on 2019-09-03

Merge branch 'master' into ChrisHughes24-patch-1

d14b917a

mergify merged 974d413b into master 6 years ago

mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone