equation_of_Z_eq_zero — Mathlib

English

If the Z-coordinate is zero, the homogeneous Weierstrass equation reduces to the affine relation y^2 = x^3.

Русский

Если Z-координата равна нулю, то удовлетворение однородного уравнения Вейерштрасса сводится к аффинному соотношению y^2 = x^3.

LaTeX

$$$W'.Equation(P) \\iff P_y^2 = P_x^3 \\quad\\text{when } P_z = 0$$$

Lean4

theorem equation_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.Equation P ↔ P y ^ 2 = P x ^ 3 := by
  simp only [equation_iff, hPz, add_zero, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _, sub_eq_zero]

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