variableChange_a₄ — Mathlib

English

Under a linear change C, the a4 coefficient transforms as a4' = u^{-4} (a4 - s a3 + 2 r a2 - (t + r s) a1 + 3 r^2 - 2 s t).

Русский

При линейном преобразовании C коэффициент a4 переходит в a4' = u^{-4} (a4 - s a3 + 2 r a2 - (t + r s) a1 + 3 r^2 - 2 s t).

LaTeX

$$$ (C \\cdot W).a_4 = C.u^{-4} \\big(W.a_4 - C.s W.a_3 + 2 C.r W.a_2 - (C.t + C.r C.s) W.a_1 + 3 C.r^2 - 2 C.s C.t\\big). $$$

Lean4

theorem variableChange_a₄ :
    (C • W).a₄ =
      C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t) :=
  rfl

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