English
If the module is nontrivial, there exists at least one nonzero ray vector.
Русский
Если модуль не тривиален, существует по крайней мере один ненулевой лучевой вектор.
LaTeX
$$$ \exists x \in \text{RayVector}(R,M). $$$
Lean4
/-- An induction principle for `Module.Ray`, used as `induction x using Module.Ray.ind`. -/
theorem ind {C : Module.Ray R M → Prop} (h : ∀ (v) (hv : v ≠ 0), C (rayOfNeZero R v hv)) (x : Module.Ray R M) : C x :=
Quotient.ind (Subtype.rec <| h) x