oangle_self — Mathlib

English

The oriented angle from x to x is zero: o.oangle(x,x) = 0.

Русский

Ориентированный угол от вектора к самому себе равен нулю: o.oangle(x,x) = 0.

LaTeX

$$$o.oangle(x,x) = 0$$$

Lean4

/-- If the two vectors passed to `oangle` are the same, the result is 0. -/
@[simp]
theorem oangle_self (x : V) : o.oangle x x = 0 :=
  by
  rw [oangle, kahler_apply_self, ← ofReal_pow]
  convert QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π))
  apply arg_ofReal_of_nonneg
  positivity

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