Mathlib v3 is deprecated. Go to Mathlib v4

Theorem projectivization.independent_pair_iff_neq

Modification history

2022-07-13 21:11
src/linear_algebra/projective_space/independence.lean
feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542) …
Added projectivization.independent_pair_iff_neqView on Github →