variableChange_Δ — Mathlib

English

Under a linear change C, the discriminant Δ scales by u^{-12}: Δ' = u^{-12} Δ.

Русский

При линейном преобразовании C дискриминант масштабируется как Δ' = u^{-12} Δ.

LaTeX

$$$ (C \\cdot W).\\Delta = C.u^{-12} W.\\Delta. $$$

Lean4

theorem variableChange_Δ : (C • W).Δ = C.u⁻¹ ^ 12 * W.Δ :=
  by
  simp only [b₂, b₄, b₆, b₈, Δ, variableChange_a₁, variableChange_a₂, variableChange_a₃, variableChange_a₄,
    variableChange_a₆]
  ring1

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