units_smul_eq_neg_iff — Mathlib

English

For any unit u and vector v, u·v = −v holds if and only if the scalar part of u is negative.

Русский

Для единичного элемента u и вектора v выполнено u·v = −v тогда и только тогда, когда скалярная часть u отрицательна.

LaTeX

$$$\text{Eq}(u\cdot v, -v) \iff u.1 < 0$$$

Lean4

@[simp]
theorem units_smul_eq_neg_iff {u : Rˣ} {v : Module.Ray R M} : u • v = -v ↔ u.1 < 0 := by
  rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg, neg_pos]

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