Inductive Projectivization.Subspace.spanCarrier

Modification history

2023-05-09 08:58

Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.lean

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

Added Projectivization.Subspace.spanCarrier View on Github →