Theorems · Inductive type · geometry

Projectivization.Subspace

(K : Type u_1) → (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Type u_2

A subspace of a projective space is a structure consisting of a set of points such that: If two nonzero vectors determine points which are in the set, and the sum of the two vectors is nonzero, then the point determined by the sum is also in the set.

Defined in

Mathlib.LinearAlgebra.Projectivization.Subspace

Cited by

34 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

DivisionRingAddCommGroupModule