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]