Commit 2022-10-05 09:32 2eac7392
View on Github →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.