Theorems · Definition · geometry

Projectivization.Subspace.span

{K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Set (Projectivization K V) → Projectivization.Subspace K V

The span of a set of points in projective space is a subspace.

Defined in: Mathlib.LinearAlgebra.Projectivization.Subspace
Cited by: 16 results in Mathlib
Foundations: Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DivisionRing AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
DivisionRingstatement and proof · cited by 1,062
Projectivizationstatement and proof · cited by 111
Projectivization.Subspacestatement · cited by 34
Projectivization.Subspace.spanCarrierproof · cited by 1

Cited by17

Results whose statement or proof uses this declaration.

Projectivization.Subspace.gistatement and proof · cited by 7
Projectivization.Subspace.span_coestatement · cited by 2
Projectivization.Subspace.span_le_subspace_iffstatement · cited by 2
Projectivization.Subspace.span_unionstatement · cited by 2
Projectivization.Subspace.subset_spanstatement · cited by 2
Projectivization.Subspace.mem_spanstatement and proof · cited by 1
Projectivization.Subspace.monotone_spanstatement · cited by 1
Projectivization.Subspace.span_emptystatement · cited by 0
Projectivization.Subspace.span_eq_of_lestatement and proof · cited by 0
Projectivization.Subspace.span_eq_sInfstatement and proof · cited by 0
Projectivization.Subspace.span_eq_span_iffstatement and proof · cited by 0
Projectivization.Subspace.span_iUnionstatement · cited by 0