mathlib3
chore(linear_algebra/basic): simplify two proofs
#2123

Merged

chore(linear_algebra/basic): simplify two proofs #2123

mergify merged 6 commits into master from submodule-directed

chore(linear_algebra/basic): simplify two proofs

dbd893f8

urkud added WIP

Fix compile

17c3ac29

urkud removed WIP

urkud added awaiting-review

Merge branch 'master' into submodule-directed

ccdee39b

jcommelin commented on 2020-03-13

jcommelin removed awaiting-review

jcommelin added awaiting-author

urkud commented on 2020-03-13

Restore `congr_right` under the name `comp_right`.

034aba32

urkud removed awaiting-author

jcommelin approved these changes on 2020-03-13

jcommelin added ready-to-merge

Merge branch 'master' into submodule-directed

7430c061

Merge branch 'master' into submodule-directed

6c1cf082

mergify merged 32c2768b into master 5 years ago

mergify deleted the submodule-directed branch 5 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone