Theorems · Definition · geometry

Projectivization.Subspace.submodule

{K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Projectivization.Subspace K V ≃o Submodule K V

The submodule corresponding to a projective subspace s, consisting of the representatives of points in s together with zero. This is the inverse of Submodule.projectivization.

Defined in

Mathlib.LinearAlgebra.Projectivization.Subspace

Cited by

8 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModule