variableChange_b₆ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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