variableChange_a₆ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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