nonsingular_add — Mathlib

English

If P1 and P2 are nonsingular and not vertically aligned in the obstruction sense, then their sum is nonsingular, following from the negAdd formula.

Русский

Если P1 и P2 невырождены и не образуют вертикальную пару, то их сумма невырождена, следуя из формулы negAdd.

LaTeX

$$(WeierstrassCurve.Affine.nonsingular_negAdd ...).mpr (WeierstrassCurve.Affine.nonsingular_neg ...)$$

Lean4

theorem nonsingular_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
    W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
  (nonsingular_neg ..).mpr <| nonsingular_negAdd h₁ h₂ hxy

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