variableChange_j — Mathlib

English

The j-invariant of a Weierstrass curve is invariant under a variable change: (C • W).j = W.j.

Русский

Инвариант j кривой Вайерштрасса сохраняется при замене переменных: (C • W).j = W.j.

LaTeX

$$$ (C \\cdot W).j = W.j $$$

Lean4

@[simp]
theorem variableChange_j : (C • W).j = W.j := by
  rw [j, coe_inv_variableChange_Δ', variableChange_c₄, j, mul_pow, ← pow_mul, ← mul_assoc,
    mul_right_comm (C.u.val ^ 12), ← mul_pow, C.u.mul_inv, one_pow, one_mul]

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