inv_def — Mathlib

English

The inverse of a linear change of variables is obtained by inverting the scale and adjusting the other parameters accordingly.

Русский

Обратное преобразование переменных получается путём взятия обратной масштабирующей величины и соответствующей перестройки остальных параметров.

LaTeX

$$$C^{-1} = \\{ u := C.u^{-1},\\; r := -C.r \\cdot C.u^{-1}{}^{2},\\; s := -C.s \\cdot C.u^{-1},\\; t := (C.r \\cdot C.s - C.t) \\cdot C.u^{-1}{}^{3} \\}.$$$

Lean4

/-- The inverse of a linear change of variables given by matrix inversion. -/
theorem inv_def :
    C⁻¹ =
      { u := C.u⁻¹
        r := -C.r * C.u⁻¹ ^ 2
        s := -C.s * C.u⁻¹
        t := (C.r * C.s - C.t) * C.u⁻¹ ^ 3 } :=
  rfl

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