mk'

Mathlib.LinearAlgebra.Projectivization.Basic

URI: https://scilib.ai/kg/mathlib#Projectivization.mk'

English

A variant of mk using a dependent pair (v) in a subtype.

Русский

Вариант mk с зависимой парой (v) в подтипе.

LaTeX

$$$ \mathrm{mk}'(K,v) = \mathrm{Quotient.mk''}(v) $$$

Lean4

/-- A variant of `Projectivization.mk` in terms of a subtype. `mk` is preferred. -/
def mk' (v : { v : V // v ≠ 0 }) : ℙ K V :=
  Quotient.mk'' v

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

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

Разделы

Аффилиация

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