equation_zero — Mathlib

English

For the projective Weierstrass curve W', the homogeneous point (0:1:0) lies on the curve, i.e., W'.Equation ![0,1,0] holds.

Русский

Для проективной кривой Вейерштрасса W' точка на бесконечности (0:1:0) лежит на кривой: W'.Equation ![0,1,0].

LaTeX

$$W'.Equation([0,1,0])$$

Lean4

theorem equation_zero : W'.Equation ![0, 1, 0] := by
  simp only [equation_of_Z_eq_zero, fin3_def_ext, zero_pow three_ne_zero]

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