Def Projectivization.Subspace.gi

Modification history

2023-05-09 08:58

Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.lean

feat port: LinearAlgebra.ProjectiveSpace.Subspace (#3832)

Added Projectivization.Subspace.gi View on Github →