someVector_ray

Mathlib.LinearAlgebra.Ray

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

← MathLib Explorer

English

The ray obtained from the representative of a ray equals the original ray.

Русский

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

LaTeX

$$$\mathrm{rayOfNeZero}(R, x.someVector) = x$$$

Lean4

/-- The ray of `someVector`. -/
@[simp]
theorem someVector_ray (x : Module.Ray R M) : rayOfNeZero R _ x.someVector_ne_zero = x :=
  (congr_arg _ (Subtype.coe_eta _ _) :).trans x.out_eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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