Def Projectivization.Subspace.span

Modification history

2023-05-09 08:58

Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.lean

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

Added Projectivization.Subspace.span View on Github →