Commit 2023-04-29 13:32 8c309869

View on Github →

feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Dfinsupp.lean

Created Mathlib/LinearAlgebra/ProjectiveSpace/Independence.lean

added inductive Projectivization.Dependent

added inductive Projectivization.Independent

added theorem Projectivization.dependent_iff

added theorem Projectivization.dependent_iff_not_independent

added theorem Projectivization.dependent_pair_iff_eq

added theorem Projectivization.independent_iff

added theorem Projectivization.independent_iff_completeLattice_independent

added theorem Projectivization.independent_iff_not_dependent

added theorem Projectivization.independent_pair_iff_neq