ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x₁ x₂ y₁ L : R<GOAL>W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L) ↔ Polynomial.eval (W.addX x₁ x₂ L) (W.addPolynomial x₁ y₁ L) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Equation x (W.negY x y)<GOAL>W.Equation x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Equation x y<GOAL>W.Equation x (W.negY x y)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Nonsingular x (W.negY x y)<GOAL>W.Nonsingular x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Nonsingular x y<GOAL>W.Nonsingular x (W.negY x y)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x₁ x₂ y₁ L : R<VAR>hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)<VAR>hx : Polynomial.eval (W.addX x₁ x₂ L) (Polynomial.derivative (W.addPolynomial x₁ y₁ L)) ≠ 0<GOAL>W.Nonsingular (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ = W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = -Polynomial.evalEval x₁ y₁ W.polynomialX / Polynomial.evalEval x₁ y₁ W.polynomialY
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hx : x₁ = x₂<GOAL>y₁ = y₂ ∨ y₁ = W.negY x₂ y₂
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>y₁ = y₂
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>Polynomial.derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) + (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ : F<VAR>y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ : F<VAR>y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ : F<VAR>y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.negY (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) = ((y₂ - W.negY x₂ y₂) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) - (y₁ - W.negY x₁ y₁) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) / (x₂ - x₁)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>WeierstrassCurve.Affine.Point.zero = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Nonsingular x y<GOAL>WeierstrassCurve.Affine.Point.some h ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>P : W.Point<GOAL>P.neg = -P
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>-0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y : R<VAR>h : W.Nonsingular x y<GOAL>-WeierstrassCurve.Affine.Point.some h = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>P Q : W.Point<GOAL>P.add Q = P + Q
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hx : x₁ = x₂<VAR>hy : y₁ = W.negY x₂ y₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>hy : y₁ = W.negY x₁ y₁<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₁ = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = -WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>hy : y₁ ≠ W.negY x₁ y₁<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₁ = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>hy : y₁ ≠ W.negY x₁ y₁<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₁ = -WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hx : x₁ ≠ x₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hx : x₁ ≠ x₂<GOAL>WeierstrassCurve.Affine.Point.some h₁ + WeierstrassCurve.Affine.Point.some h₂ = -WeierstrassCurve.Affine.Point.some ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W f).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom f) W.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>Polynomial.evalEval (Polynomial.C Polynomial.X) Y (WeierstrassCurve.baseChange W R[X][Y]).toAffine.polynomial = W.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : R<VAR>h : W.Equation x y<GOAL>WeierstrassCurve.Affine.Equation (WeierstrassCurve.map W f) (f x) (f y)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R<GOAL>(WeierstrassCurve.map W f).toAffine.Equation (f x) (f y) ↔ W.Equation x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W f).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom f) W.polynomialX
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W f).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom f) W.polynomialY
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x y : R<GOAL>(WeierstrassCurve.map W f).toAffine.Nonsingular (f x) (f y) ↔ W.Nonsingular x y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W f).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W.negPolynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : R<GOAL>(WeierstrassCurve.map W f).toAffine.negY (f x) (f y) = f (W.negY x y)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x y L : R<GOAL>WeierstrassCurve.Affine.linePolynomial (f x) (f y) (f L) = Polynomial.map f (WeierstrassCurve.Affine.linePolynomial x y L)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x y L : R<GOAL>(WeierstrassCurve.map W f).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map f (W.addPolynomial x y L)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ L : R<GOAL>(WeierstrassCurve.map W f).toAffine.addX (f x₁) (f x₂) (f L) = f (W.addX x₁ x₂ L)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>(WeierstrassCurve.map W f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f (W.negAddY x₁ x₂ y₁ L)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>(WeierstrassCurve.map W f).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.toAffine W).addY x₁ x₂ y₁ L)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>K : Type v<VAR>Field K<VAR>f : F →+* K<VAR>x₁ x₂ y₁ y₂ : F<GOAL>(WeierstrassCurve.map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(WeierstrassCurve.baseChange W B).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (WeierstrassCurve.baseChange W A).toAffine.polynomial
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.Equation (f x) (f y) ↔ (WeierstrassCurve.baseChange W A).toAffine.Equation x y
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(WeierstrassCurve.baseChange W B).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom ↑f) (WeierstrassCurve.baseChange W A).toAffine.polynomialX
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(WeierstrassCurve.baseChange W B).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom ↑f) (WeierstrassCurve.baseChange W A).toAffine.polynomialY
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>hf : Function.Injective ⇑f<VAR>x y : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.Nonsingular (f x) (f y) ↔ (WeierstrassCurve.baseChange W A).toAffine.Nonsingular x y
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(WeierstrassCurve.baseChange W B).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (WeierstrassCurve.baseChange W A).toAffine.negPolynomial
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.negY (f x) (f y) = f ((WeierstrassCurve.baseChange W A).toAffine.negY x y)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x y L : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map (↑f) ((WeierstrassCurve.baseChange W A).toAffine.addPolynomial x y L)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ L : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.addX (f x₁) (f x₂) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.addX x₁ x₂ L)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.negAddY x₁ x₂ y₁ L)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : Type v<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ y₁ L : A<GOAL>(WeierstrassCurve.baseChange W B).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.addY x₁ x₂ y₁ L)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>Algebra S F<VAR>IsScalarTower R S F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>Algebra S K<VAR>IsScalarTower R S K<VAR>f : F →ₐ[S] K<VAR>x₁ x₂ y₁ y₂ : F<GOAL>(WeierstrassCurve.baseChange W K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((WeierstrassCurve.baseChange W F).toAffine.slope x₁ x₂ y₁ y₂)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>Algebra S F<VAR>IsScalarTower R S F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>Algebra S K<VAR>IsScalarTower R S K<VAR>f : F →ₐ[S] K<GOAL>(WeierstrassCurve.Affine.Point.map W f) 0 = 0
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>Algebra S F<VAR>IsScalarTower R S F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>Algebra S K<VAR>IsScalarTower R S K<VAR>f : F →ₐ[S] K<VAR>x y : F<VAR>h : (WeierstrassCurve.baseChange W F).toAffine.Nonsingular x y<GOAL>(WeierstrassCurve.Affine.Point.map W f) (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Affine.Point.some ⋯
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>P : WeierstrassCurve.Affine.Point (WeierstrassCurve.baseChange W F)<GOAL>(WeierstrassCurve.Affine.Point.map W (Algebra.ofId F F)) P = P
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>Algebra S F<VAR>IsScalarTower R S F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>Algebra S K<VAR>IsScalarTower R S K<VAR>f : F →ₐ[S] K<VAR>L : Type w<VAR>Field L<VAR>Algebra R L<VAR>Algebra S L<VAR>IsScalarTower R S L<VAR>g : K →ₐ[S] L<VAR>P : WeierstrassCurve.Affine.Point (WeierstrassCurve.baseChange W F)<GOAL>(WeierstrassCurve.Affine.Point.map W g) ((WeierstrassCurve.Affine.Point.map W f) P) = (WeierstrassCurve.Affine.Point.map W (g.comp f)) P
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>S : Type s<VAR>CommRing S<VAR>Algebra R S<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>Algebra S F<VAR>IsScalarTower R S F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>Algebra S K<VAR>IsScalarTower R S K<VAR>f : F →ₐ[S] K<GOAL>Function.Injective ⇑(WeierstrassCurve.Affine.Point.map W f)
<VAR>R : Type r<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>F : Type u<VAR>Field F<VAR>Algebra R F<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>L : Type w<VAR>Field L<VAR>Algebra R L<VAR>Algebra F K<VAR>IsScalarTower R F K<VAR>Algebra F L<VAR>IsScalarTower R F L<VAR>f : K →ₐ[F] L<VAR>P : WeierstrassCurve.Affine.Point (WeierstrassCurve.baseChange W F)<GOAL>(WeierstrassCurve.Affine.Point.map W f) ((WeierstrassCurve.Affine.Point.baseChange W F K) P) = (WeierstrassCurve.Affine.Point.baseChange W F L) P
<VAR>R : Type u<VAR>CommRing R<VAR>E : EllipticCurve R<VAR>Nontrivial R<VAR>x y : R<VAR>h : E.toAffine.Equation x y<GOAL>E.toAffine.Nonsingular x y
<VAR>α : Type u<VAR>s t : Set α<VAR>ht : t.Subsingleton<VAR>hst : s ⊆ t<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>x : α<VAR>hx : x ∈ s<GOAL>s = {x}
<VAR>α : Type u<VAR>a : α<GOAL>{a}.Subsingleton
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>h : s ⊆ {a}<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : ∀ b ∈ s, b = a<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.Subsingleton ↔ s = {x}
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s = ∅ ∨ ∃ x, s = {x}
<VAR>α : Type u<VAR>s : Set α<VAR>p : Set α → Prop<VAR>hs : s.Subsingleton<VAR>he : p ∅<VAR>h₁ : ∀ (x : α), p {x}<GOAL>p s
<VAR>α : Type u<VAR>Subsingleton α<GOAL>Set.univ.Subsingleton
<VAR>α : Type u<VAR>h : Set.univ.Subsingleton<GOAL>Subsingleton α
<VAR>α : Type u<GOAL>Set.univ.Subsingleton ↔ Subsingleton α
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>(s ∩ {a}).Subsingleton
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>({a} ∩ s).Subsingleton
<VAR>α : Type u<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.Subsingleton
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsTop x}.Subsingleton
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsBot x}.Subsingleton
<VAR>α : Type u<VAR>s : Set α<GOAL>(∃ a, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<GOAL>Subsingleton ↑s ↔ s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Subsingleton → Subsingleton ↑s
<VAR>α : Type u<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>hs.choose.1 ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>hs.choose.2 ∈ s
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>hs.choose.1 ≠ hs.choose.2
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Nontrivial<VAR>hst : s ⊆ t<GOAL>t.Nontrivial
<VAR>α : Type u<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>x y : α<VAR>hxy : x ≠ y<VAR>h : {x, y} ⊆ s<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>∃ x y, x ≠ y ∧ {x, y} ⊆ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nontrivial ↔ ∃ x y, x ≠ y ∧ {x, y} ⊆ s
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>h : ∃ y ∈ s, y ≠ x<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<VAR>z : α<GOAL>∃ x ∈ s, x ≠ z
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.Nontrivial ↔ ∃ y ∈ s, y ≠ x
<VAR>α : Type u<VAR>s : Set α<VAR>Preorder α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x < y<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>Preorder α<VAR>H : ∃ x ∈ s, ∃ y ∈ s, x < y<GOAL>s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>LinearOrder α<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x < y
<VAR>α : Type u<VAR>s : Set α<VAR>LinearOrder α<GOAL>s.Nontrivial ↔ ∃ x ∈ s, ∃ y ∈ s, x < y
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.Nonempty
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s ≠ ∅
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>¬s ⊆ ∅
<VAR>α : Type u<GOAL>¬∅.Nontrivial
<VAR>α : Type u<VAR>x : α<GOAL>¬{x}.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hs : s.Nontrivial<GOAL>s ≠ {x}
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<VAR>hs : s.Nontrivial<GOAL>¬s ⊆ {x}
<VAR>α : Type u<VAR>Nontrivial α<GOAL>Set.univ.Nontrivial
<VAR>α : Type u<VAR>h : Set.univ.Nontrivial<GOAL>Nontrivial α
<VAR>α : Type u<GOAL>Set.univ.Nontrivial ↔ Nontrivial α
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>Nontrivial α
<VAR>α : Type u<VAR>s : Set α<GOAL>Nontrivial ↑s ↔ s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<VAR>hs : Nontrivial ↑s<GOAL>Nontrivial α
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>hs : Nontrivial ↑s<GOAL>Nontrivial ↑t
<VAR>α : Type u<VAR>s : Set α<GOAL>¬s.Subsingleton ↔ s.Nontrivial
<VAR>α : Type u<VAR>s : Set α<GOAL>¬s.Nontrivial ↔ s.Subsingleton
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Subsingleton ∨ s.Nontrivial
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>ha : a ∈ s<GOAL>s = {a} ∨ s.Nontrivial
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<VAR>ha : a ∈ s<GOAL>s.Nontrivial ↔ s ≠ {a}
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : s.Subsingleton<GOAL>MonotoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : s.Subsingleton<GOAL>AntitoneOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>h : s.Subsingleton<GOAL>StrictMonoOn f s