units_smul_eq_self_iff — Mathlib

English

For any unit u of R and any vector v in Module.Ray R M, we have u•v = v if and only if the underlying scalar u has positive value.

Русский

Для любого единичного элемента u в кольце R и любого вектора v в Module.Ray R M выполняется u·v = v тогда и только тогда, когда соответствующее число u > 0.

LaTeX

$$$\bigl(u\cdot v = v\bigr) \iff 0 < (u: R)$$$

Lean4

@[simp]
theorem units_smul_eq_self_iff {u : Rˣ} {v : Module.Ray R M} : u • v = v ↔ 0 < (u : R) := by
  induction v using Module.Ray.ind with
  | h v hv => simp only [smul_rayOfNeZero, ray_eq_iff, Units.smul_def, sameRay_smul_left_iff_of_ne hv u.ne_zero]

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