of_subsingleton' — Mathlib

English

If the coefficient ring is a subsingleton, then any two vectors in any module are on the same ray.

Русский

Если кольцо-коэффициент подсинглтон, то любые два вектора в любом модуле лежат на одном луче.

LaTeX

$$$[Subsingleton R] \\Rightarrow \\forall M,[Module R M], \\forall x,y: M, SameRay R x y$$$

Lean4

@[nontriviality]
theorem of_subsingleton' [Subsingleton R] (x y : M) : SameRay R x y :=
  haveI := Module.subsingleton R M
  of_subsingleton x y

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