Commit 2023-05-09 08:58 3e2a20e9

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/ProjectiveSpace/Subspace.lean

added def Projectivization.Subspace.gi

added theorem Projectivization.Subspace.mem_add

added theorem Projectivization.Subspace.mem_carrier_iff

added theorem Projectivization.Subspace.mem_span

added theorem Projectivization.Subspace.monotone_span

added def Projectivization.Subspace.span

added inductive Projectivization.Subspace.spanCarrier

added theorem Projectivization.Subspace.span_coe

added theorem Projectivization.Subspace.span_empty

added theorem Projectivization.Subspace.span_eq_infₛ

added theorem Projectivization.Subspace.span_eq_of_le

added theorem Projectivization.Subspace.span_eq_span_iff

added theorem Projectivization.Subspace.span_le_subspace_iff

added theorem Projectivization.Subspace.span_sup

added theorem Projectivization.Subspace.span_union

added theorem Projectivization.Subspace.span_unionᵢ

added theorem Projectivization.Subspace.span_univ

added theorem Projectivization.Subspace.subset_span

added theorem Projectivization.Subspace.subset_span_trans

added theorem Projectivization.Subspace.sup_span

added structure Projectivization.Subspace