oangle_neg_right — Mathlib

English

If x ≠ 0 and y ≠ 0, then o.oangle x (-y) = o.oangle x y + π.

Русский

Если x ≠ 0 и y ≠ 0, тогда o.oangle x(-y) = o.oangle x y + π.

LaTeX

$$$x \neq 0 \land y \neq 0 \Rightarrow o.oangle\;x(-y) = o.oangle\;x\;y + \pi$$$

Lean4

/-- Negating the second vector passed to `oangle` adds `π` to the angle. -/
theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x (-y) = o.oangle x y + π :=
  by
  simp only [oangle, map_neg]
  convert Complex.arg_neg_coe_angle _
  exact o.kahler_ne_zero hx hy

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