Theorems · Definition · geometry

Projectivization.mk

(K : Type u_1) →
  {V : Type u_2} →
    [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (v : V) → v ≠ 0 → Projectivization K V

Construct an element of the projectivization from a nonzero vector.

Defined in: Mathlib.LinearAlgebra.Projectivization.Basic
Cited by: 55 results in Mathlib
Foundations: Depth 68 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.

Cites5

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

Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
DivisionRingstatement and proof · cited by 1,062
Quotient.mk''proof · cited by 132
Projectivizationstatement · cited by 111

Cited by69

Results whose statement or proof uses this declaration.

Projectivization.indstatement and proof · cited by 15
Projectivization.mk_repstatement · cited by 8
Projectivization.Subspace.submoduleproof · cited by 8
OnePoint.equivProjectivizationproof · cited by 7
Projectivization.mk_eq_mk_iff_crossProduct_eq_zerostatement · cited by 5
Projectivization.mk_eq_mk_iffstatement · cited by 4
Projectivization.independent_iffproof · cited by 3
Projectivization.mk_eq_mk_iff'statement · cited by 3
Projectivization.submodule_mkstatement · cited by 3
Projectivization.mk.congr_simpstatement and proof · cited by 3
OnePoint.equivProjectivization_symm_apply_mkstatement and proof · cited by 3
Projectivization.independent_mk_iff_LinearIndependentstatement and proof · cited by 2