Theorems · Theorem · algebraic geometry

WeierstrassCurve.Jacobian.add_smul_of_not_equiv

∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  ¬P ≈ Q → ∀ {u v : R}, IsUnit u → IsUnit v → W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing