rayOfNeZero

Mathlib.LinearAlgebra.Ray

URI: https://scilib.ai/kg/mathlib#rayOfNeZero

English

The ray determined by a nonzero vector is an element of the ray space.

Русский

Луч, определяемый ненулевым вектором, является элементом пространства лучей.

LaTeX

$$$ \text{rayOfNeZero}(R, v, v\neq 0) \in \operatorname{Module.Ray}(R, M). $$$

Lean4

/-- The ray given by a nonzero vector. -/
def rayOfNeZero (v : M) (h : v ≠ 0) : Module.Ray R M :=
  ⟦⟨v, h⟩⟧

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

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

Разделы

Аффилиация

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