mathlib
6857dc50 - bug(linear_algebra/*): Fix sorry and remove duplicate lemma

Commit

5 years ago

bug(linear_algebra/*): Fix sorry and remove duplicate lemma

Author

eric-wieser

eric-wieser

Parents

Loading