Commit 2022-07-13 21:11 1e82f5ec

View on Github →

feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542) This PR only provides definitions and basic lemmas. In an upcoming pull request we use this to prove the axioms for an abstract projective space.

Estimated changes

Modified src/linear_algebra/projective_space/basic.lean

added theorem projectivization.mk_eq_mk_iff'

Created src/linear_algebra/projective_space/independence.lean

added inductive projectivization.dependent

added theorem projectivization.dependent_iff

added theorem projectivization.dependent_iff_not_independent

added theorem projectivization.dependent_pair_iff_eq

added inductive projectivization.independent

added theorem projectivization.independent_iff

added theorem projectivization.independent_iff_complete_lattice_independent

added theorem projectivization.independent_iff_not_dependent

added theorem projectivization.independent_pair_iff_neq