Commit 2023-04-29 09:57 7b53c836

View on Github →

feat: port LinearAlgebra.ProjectiveSpace.Basic (#3692)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/ProjectiveSpace/Basic.lean

added theorem Projectivization.exists_smul_eq_mk_rep

added theorem Projectivization.finrank_submodule

added theorem Projectivization.ind

added def Projectivization.map

added theorem Projectivization.map_comp

added theorem Projectivization.map_id

added theorem Projectivization.map_injective

added theorem Projectivization.map_mk

added theorem Projectivization.mk''_submodule

added def Projectivization.mk'

added theorem Projectivization.mk'_eq_mk

added def Projectivization.mk

added theorem Projectivization.mk_eq_mk_iff'

added theorem Projectivization.mk_eq_mk_iff

added theorem Projectivization.mk_rep

added theorem Projectivization.rep_nonzero

added theorem Projectivization.submodule_eq

added theorem Projectivization.submodule_injective

added theorem Projectivization.submodule_mk''

added theorem Projectivization.submodule_mk

added def Projectivization

added def projectivizationSetoid