ind — Mathlib

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

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