variableChange_b₄ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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