mk'' — Mathlib

English

From a 1-dimensional subspace H of V, one can construct a point of the projective space by mk''(H,h).

Русский

Из однодиапазонного подпространства H в V строится точка проективного пространства через mk''(H,h).

LaTeX

$$mk''(H,h) ∈ \mathbb{P}_K(V)$$

Lean4

/-- Construct an element of the projectivization from a subspace of dimension 1. -/
noncomputable def mk'' (H : Submodule K V) (h : finrank K H = 1) : ℙ K V :=
  (equivSubmodule K V).symm ⟨H, h⟩

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