stereoInvFunAux_apply — Mathlib

English

For any w in E, stereoInvFunAux v w equals the explicit algebraic expression (‖w‖^2 + 4)^{-1} times ((4) w + (‖w‖^2 - 4) v).

Русский

Для любого w в E stereoInvFunAux v w равно явному алгебраическому выражению (‖w‖^2 + 4)^{-1} умноженному на ((4) w + (‖w‖^2 - 4) v).

LaTeX

$$stereoInvFunAux\ v\ w = (\|w\|^2 + 4)^{-1} \cdot (4 w + (\|w\|^2 - 4) v)$$

Lean4

@[simp]
theorem stereoInvFunAux_apply (w : E) : stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • ((4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v) :=
  rfl

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