instNonemptyRayVectorOfNontrivial

Mathlib.LinearAlgebra.Ray

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

English

If the module is nontrivial, there exists at least one ray vector.

Русский

Если модуль не тривиален, то существует по крайней мере один вектор в луче.

LaTeX

$$$\exists \; \text{RayVector } R M.$$$

Lean4

instance {R M : Type*} [Zero M] [Nontrivial M] : Nonempty (RayVector R M) :=
  let ⟨x, hx⟩ := exists_ne (0 : M)
  ⟨⟨x, hx⟩⟩

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

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

Разделы

Аффилиация

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