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