angle_smul_left_of_pos — Mathlib

English

If r > 0, then the angle between r x and y equals the angle between x and y.

Русский

Если r > 0, то угол между r x и y равен углу между x и y.

LaTeX

$$$\\\\angle (r \\cdot x) y = \\\\angle x y$ при $r>0$$$

Lean4

/-- The angle between a positive multiple of a vector and a vector. -/
@[simp]
theorem angle_smul_left_of_pos (x y : V) {r : ℝ} (hr : 0 < r) : angle (r • x) y = angle x y := by
  rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]

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