English
Let o be an orientation on a 2-dimensional real inner product space V. For all x, y in V and all nonzero real r, doubling the oriented angle from x to r y equals doubling the oriented angle from x to y; i.e., 2·oangle(x, r y) = 2·oangle(x, y).
Русский
Пусть o — ориентированность на двумерном вещественном внутреннем произведении пространстве V. Для любых x, y в V и любого ненулевого вещественного числа r выполняется равенство: удвоенный ориентированный угол между x и r y равен удвоенному углу между x и y; то есть 2·oangle(x, r y) = 2·oangle(x, y).
LaTeX
$$$ (2) \cdot \mathrm{oangle}(x, r y) = (2) \cdot \mathrm{oangle}(x, y) $$$
Lean4
/-- Multiplying the second vector passed to `oangle` by a nonzero real does not change twice the
angle. -/
@[simp]
theorem two_zsmul_oangle_smul_right_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) :
(2 : ℤ) • o.oangle x (r • y) = (2 : ℤ) • o.oangle x y := by rcases hr.lt_or_gt with (h | h) <;> simp [h]
