mathlib
a012d76d - chore(linear_algebra/projection): use implicit args in lemmas (#2773)

Commit

5 years ago

chore(linear_algebra/projection): use implicit args in lemmas (#2773)

Author

urkud

urkud

Parents

Loading