someVector_ne_zero

Mathlib.LinearAlgebra.Ray

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

English

The chosen representative of a ray is nonzero.

Русский

Выбранный представитель луча ненулевой.

LaTeX

$$$x.\text{someVector} \neq 0$$$

Lean4

/-- `someVector` is nonzero. -/
@[simp]
theorem someVector_ne_zero (x : Module.Ray R M) : x.someVector ≠ 0 :=
  x.someRayVector.property

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

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

Разделы

Аффилиация

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