two_zsmul_oangle_smul_left_of_ne_zero

English

If r ≠ 0 then 2 · o.oangle (r·x) y = 2 · o.oangle x y.

Русский

Если r ≠ 0, тогда 2 · o.oangle (r·x) y = 2 · o.oangle x y.

LaTeX

$$$r \neq 0 \Rightarrow 2\,o.oangle (r\cdot x)\;y = 2\,o.oangle x\;y$$$

Lean4

/-- Multiplying the first vector passed to `oangle` by a nonzero real does not change twice the
angle. -/
@[simp]
theorem two_zsmul_oangle_smul_left_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) :
    (2 : ℤ) • o.oangle (r • x) y = (2 : ℤ) • o.oangle x y := by rcases hr.lt_or_gt with (h | h) <;> simp [h]

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