rep

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.rep

English

Choose a representative of a projective class in V.

Русский

Выбрать представителя класса в V.

LaTeX

$$$ \mathrm{rep} : \mathbb{P}_K V \to V $$$

Lean4

/-- Choose a representative of `v : Projectivization K V` in `V`. -/
protected noncomputable def rep (v : ℙ K V) : V :=
  v.out

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru