someVector

Mathlib.LinearAlgebra.Ray

URI: https://scilib.ai/kg/mathlib#Module.Ray.someVector

English

Each Module.Ray comes from some nonzero vector via the underlying ray construction.

Русский

Каждый луч в Module.Ray порождается некоторым ненулевым вектором через соответствующее строение луча.

LaTeX

$$$\text{someVector}(x) = \text{the underlying vector of } x.$$$

Lean4

/-- An arbitrary nonzero vector giving a ray. -/
def someVector (x : Module.Ray R M) : M :=
  x.someRayVector

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

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

Разделы

Аффилиация

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