Theorems · Theorem · algebraic geometry

WeierstrassCurve.Projective.add_smul_of_equiv

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

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing