mul_def — Mathlib

English

The composition of two linear changes of variables is again a linear change, with parameters given by the product and certain sums involving the original parameters.

Русский

Сложение двух линейных преобразований переменных снова дает линейное преобразование; новые параметры задаются произведениями и определенными суммами исходных параметров.

LaTeX

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

Lean4

/-- The composition of two linear changes of variables given by matrix multiplication. -/
theorem mul_def :
    C * C' =
      { u := C.u * C'.u
        r := C.r * C'.u ^ 2 + C'.r
        s := C'.u * C.s + C'.s
        t := C.t * C'.u ^ 3 + C.r * C'.s * C'.u ^ 2 + C'.t } :=
  rfl

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