English
The angle between nonzero vectors x and y equals θ if and only if y equals the rotation of x by θ scaled by the ratio of their norms.
Русский
Угол между не нулевыми векторами x и y равен θ тогда и только тогда, когда y равен повороту x на θ, умноженному на коэффициент ‖y‖/‖x‖.
LaTeX
$$o.oangle x y = θ \iff y = (‖y‖ / ‖x‖) • o.rotation θ x \text{ при } x ≠ 0, y ≠ 0$$
Lean4
/-- The angle between two nonzero vectors is `θ` if and only if the second vector is the first
rotated by `θ` and scaled by the ratio of the norms. -/
theorem oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) :
o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • o.rotation θ x :=
by
have hp := div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx)
constructor
· rintro rfl
rw [← LinearIsometryEquiv.map_smul, ← o.oangle_smul_left_of_pos x y hp, eq_comm, rotation_oangle_eq_iff_norm_eq,
norm_smul, Real.norm_of_nonneg hp.le, div_mul_cancel₀ _ (norm_ne_zero_iff.2 hx)]
· intro hye
rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]
