secondInter_smul — Mathlib

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]

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