neg_units_smul — Mathlib

English

Negating a ray and multiplying by a unit is compatible: -u · v = -(u · v).

Русский

Отрицание луча и умножение на единицу согласованы: -u · v = -(u · v).

LaTeX

$$$-u\cdot v = -(u\cdot v)$ for unit $u$.$$

Lean4

theorem neg_units_smul (u : Rˣ) (v : Module.Ray R M) : -u • v = -(u • v) :=
  by
  induction v using Module.Ray.ind
  simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

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