Theorems · Definition · geometry

Submodule.projectivization

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

The projective subspace corresponding to a submodule s, consisting of the one-dimensional subspaces of s. This is the inverse of Projectivization.Subspace.submodule.

Defined in

Mathlib.LinearAlgebra.Projectivization.Subspace

Cited by

6 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModule