mathlib
2eac7392 - feat(linear_algebra/affine_space/finite_dimensional): `collinear` lemmas, implicit arguments (#16332)

Commit
3 years ago
feat(linear_algebra/affine_space/finite_dimensional): `collinear` lemmas, implicit arguments (#16332) Add more lemmas about `collinear`, and change existing `iff` lemmas about `collinear` to follow usual mathlib conventions about implicit arguments for such lemmas.
Author
Parents
Loading