add — Mathlib

English

A refined form of the degree inequality for the norm in the coordinate ring; the degree is never 1 for any coordinate ring element, mirroring the prior result.

Русский

Уточненная форма неравенства степеней нормы в координатном кольце: степень никогда не равна 1.

LaTeX

$$$\\deg(\\operatorname{norm}_{R[X]}(x)) \\neq 1$$$

Lean4

/-- The addition of two nonsingular points on a Weierstrass curve in affine coordinates.

Given two nonsingular points `P` and `Q` in affine coordinates, use `P + Q` instead of `add P Q`. -/
def add [DecidableEq F] : W.Point → W.Point → W.Point
  | 0, P => P
  | P, 0 => P
  | @some _ _ _ x₁ y₁ h₁, @some _ _ _ x₂ y₂ h₂ =>
    if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else some <| nonsingular_add h₁ h₂ hxy

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