units_smul_of_neg — Mathlib

English

If a unit has negative value, negating its smul is the same as smul by the negated unit.

Русский

Если значение единицы отрицательно, то отрицание умножения на единицу эквивалентно умножению на отрицательную единицу.

LaTeX

$$$-u\cdot v = -(u\cdot v)$ when $u<0$.$$

Lean4

/-- Scaling by a negative unit is negation. -/
theorem units_smul_of_neg (u : Rˣ) (hu : (u : R) < 0) (v : Module.Ray R M) : u • v = -v :=
  by
  rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]
  rwa [Units.val_neg, Right.neg_pos_iff]

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