mk — Mathlib · SciLib

English

A function on nonzero vectors that is invariant under scaling descends to a function on the projectivization.

Русский

Функция на ненулевых векторах, инвариантная к масштабированию, нисходит на проективное пространство.

LaTeX

$$$ \text{lift} : (\{ v : V \mid v \neq 0 \} \to \alpha) \to (\mathbb{P}_K V \to \alpha) $ and the descent is possible if hf holds.$$

Lean4

/-- Construct an element of the projectivization from a nonzero vector. -/
def mk (v : V) (hv : v ≠ 0) : ℙ K V :=
  Quotient.mk'' ⟨v, hv⟩

Похожие утверждения