English
SecondInter is invariant under nonzero scaling of the direction vector.
Русский
SecondInter неизменен при умножении направления на ненулевой скаляр.
LaTeX
$$$s.secondInter(p, r\\cdot v) = s.secondInter(p,v)$ for r \\neq 0$$
Lean4
/-- `secondInter` is unchanged by multiplying the vector by a nonzero real. -/
@[simp]
theorem secondInter_smul (s : Sphere P) (p : P) (v : V) {r : ℝ} (hr : r ≠ 0) :
s.secondInter p (r • v) = s.secondInter p v :=
by
simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul, div_mul_eq_div_div]
rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
mul_div_cancel_left₀ _ hr, mul_comm]