variableChange_b₈ — Mathlib

English

Under a linear change C, the b8 coefficient transforms as b8' = u^{-8} (b8 + 3 r b6 + 3 r^2 b4 + r^3 b2 + 3 r^4).

Русский

При линейном преобразовании C коэффициент b8 переходит в b8' = u^{-8} (b8 + 3 r b6 + 3 r^2 b4 + r^3 b2 + 3 r^4).

LaTeX

$$$ (C \\cdot W).b_8 = C.u^{-8} \\big(W.b_8 + 3 C.r W.b_6 + 3 C.r^2 W.b_4 + C.r^3 W.b_2 + 3 C.r^4\\big). $$$

Lean4

theorem variableChange_b₈ :
    (C • W).b₈ = C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4) :=
  by
  simp only [b₂, b₄, b₆, b₈, variableChange_a₁, variableChange_a₂, variableChange_a₃, variableChange_a₄,
    variableChange_a₆]
  ring1

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