ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>W'.neg P ≈ W'.neg Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.neg P = ![P x, -P y, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>W.neg P = -(P y / P x) • ![1, 1, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<GOAL>W.Nonsingular ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<GOAL>W.Nonsingular (W.neg P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addZ P (W'.neg P) = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addX P (W'.neg P) = W'.dblZ P ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addY P (W'.neg P) = -W'.dblZ P ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.negMap ⟦P⟧ = ⟦W'.neg P⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.negMap ⟦P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : WeierstrassCurve.Jacobian.PointClass F<VAR>hP : W.NonsingularLift P<GOAL>W.NonsingularLift (W.negMap P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>W'.add P Q = W'.dblXYZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.add P P = W'.dblXYZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P = Q<GOAL>W'.add P Q = W'.dblXYZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : ¬P ≈ Q<GOAL>W'.add P Q = W'.addXYZ P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : ¬P ≈ Q<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>u v : R<VAR>hu : IsUnit u<VAR>hv : IsUnit v<GOAL>W'.add (u • P) (v • Q) ≈ W'.add P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P P' Q Q' : Fin 3 → R<VAR>hP : P ≈ P'<VAR>hQ : Q ≈ Q'<GOAL>W'.add P Q ≈ W'.add P' Q'
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<GOAL>W.add P Q = P x ^ 2 • ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<VAR>hQz : Q z ≠ 0<GOAL>W'.add P Q = (P x * Q z) • Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z = 0<GOAL>W'.add P Q = -(Q x * P z) • P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.add P Q = W.dblU P • ![1, 1, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>W.add P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.add P Q = W.dblZ P • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.add P Q = WeierstrassCurve.Jacobian.addZ P Q • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hxy : P x * Q z ^ 2 = Q x * P z ^ 2 → P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.Nonsingular ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<GOAL>W.Nonsingular (W.add P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<GOAL>W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>Q : WeierstrassCurve.Jacobian.PointClass F<VAR>hP : W.Nonsingular P<VAR>hQ : W.NonsingularLift Q<VAR>hPz : P z = 0<GOAL>W.addMap ⟦P⟧ Q = Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : WeierstrassCurve.Jacobian.PointClass F<VAR>Q : Fin 3 → F<VAR>hP : W.NonsingularLift P<VAR>hQ : W.Nonsingular Q<VAR>hQz : Q z = 0<GOAL>W.addMap P ⟦Q⟧ = P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hxy : P x * Q z ^ 2 = Q x * P z ^ 2 → P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]⟧
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : WeierstrassCurve.Jacobian.PointClass F<VAR>hP : W.NonsingularLift P<VAR>hQ : W.NonsingularLift Q<GOAL>W.NonsingularLift (W.addMap P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>self : W'.Point<GOAL>W'.NonsingularLift self.point
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : WeierstrassCurve.Jacobian.PointClass R<VAR>h : W'.NonsingularLift P<GOAL>(WeierstrassCurve.Jacobian.Point.mk h).point = P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<GOAL>0 = WeierstrassCurve.Jacobian.Point.mk ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<GOAL>WeierstrassCurve.Jacobian.Point.point 0 = ⟦![1, 1, 0]⟧
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<GOAL>WeierstrassCurve.Jacobian.Point.fromAffine 0 = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<VAR>X Y : R<VAR>h : W'.toAffine.Nonsingular X Y<GOAL>WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) = WeierstrassCurve.Jacobian.Point.mk ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<VAR>X Y : R<VAR>h : W'.toAffine.Nonsingular X Y<GOAL>WeierstrassCurve.Jacobian.Point.fromAffine (WeierstrassCurve.Affine.Point.some h) ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : W.Point<GOAL>-P = P.neg
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : W.Point<GOAL>(-P).point = W.negMap P.point
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : W.Point<GOAL>P + Q = P.add Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : W.Point<GOAL>(P + Q).point = W.addMap P.point Q.point
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : ¬W.Nonsingular P<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W P = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z = 0<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W P = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W ![1, 1, 0] = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>X Y : F<VAR>h : W.Nonsingular ![X, Y, 1]<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W ![X, Y, 1] = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>u : F<VAR>hu : IsUnit u<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W (u • P) = WeierstrassCurve.Jacobian.Point.toAffine W P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>h : P ≈ Q<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Jacobian.Point.toAffine W Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W (W.neg P) = -WeierstrassCurve.Jacobian.Point.toAffine W P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hxy : P x * Q z ^ 2 = Q x * P z ^ 2 → P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1] = WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<GOAL>WeierstrassCurve.Jacobian.Point.toAffine W (W.add P Q) = WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.NonsingularLift ⟦P⟧<GOAL>(WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = WeierstrassCurve.Jacobian.Point.toAffine W P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.NonsingularLift ⟦P⟧<VAR>hPz : P z = 0<GOAL>(WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<GOAL>WeierstrassCurve.Jacobian.Point.toAffineLift 0 = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.NonsingularLift ⟦P⟧<VAR>hPz : P z ≠ 0<GOAL>(WeierstrassCurve.Jacobian.Point.mk hP).toAffineLift = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>X Y : F<VAR>h : W.NonsingularLift ⟦![X, Y, 1]⟧<GOAL>(WeierstrassCurve.Jacobian.Point.mk h).toAffineLift = WeierstrassCurve.Affine.Point.some ⋯
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : W.Point<GOAL>(-P).toAffineLift = -P.toAffineLift
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : W.Point<GOAL>(P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : W.Point<GOAL>(WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W) P = P.toAffineLift
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<GOAL>∀ (a : W.toAffine.Point), (WeierstrassCurve.Jacobian.Point.toAffineAddEquiv W).symm a = WeierstrassCurve.Jacobian.Point.fromAffine a
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<VAR>u : R<GOAL>⇑f ∘ (u • P) = f u • ⇑f ∘ P
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addZ (⇑f ∘ P) (⇑f ∘ Q) = f (WeierstrassCurve.Jacobian.addZ P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addX (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addX P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.negAddY (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.negAddY P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.negY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.negY P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.neg (WeierstrassCurve.map W' f) (⇑f ∘ P) = ⇑f ∘ W'.neg P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addY (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addXYZ (WeierstrassCurve.map W' f) (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W' f).toJacobian.polynomial = (MvPolynomial.map f) W'.polynomial
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<GOAL>(WeierstrassCurve.map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.dblZ (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblZ P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.dblU (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblU P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.dblX (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblX P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.negDblY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.negDblY P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.dblY (WeierstrassCurve.map W' f) (⇑f ∘ P) = f (W'.dblY P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>S : Type u_1<VAR>CommRing S<VAR>f : R →+* S<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.dblXYZ (WeierstrassCurve.map W' f) (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
<VAR>r : ℝ<VAR>tr : Transcendental ℚ r<GOAL>Irrational r
<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>hxr : x ^ n = ↑m<VAR>hv : ¬∃ y, x = ↑y<VAR>hnpos : 0 < n<GOAL>Irrational x
<VAR>m : ℤ<VAR>hm : 0 < m<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>Hpv : (multiplicity (↑p) m).get ⋯ % 2 = 1<GOAL>Irrational √↑m
<VAR>q : ℚ<VAR>hq : 0 ≤ q<GOAL>Irrational √↑q ↔ ¬IsSquare q
<VAR>q : ℚ<GOAL>Irrational √↑q ↔ ¬IsSquare q ∧ 0 ≤ q
<VAR>n : ℕ<GOAL>Irrational √↑n ↔ ¬IsSquare n
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Irrational √(OfNat.ofNat n) ↔ ¬IsSquare (OfNat.ofNat n)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>Irrational √↑p
<VAR>x : ℝ<VAR>h : Irrational x<VAR>q : ℚ<GOAL>x ≠ ↑q
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<GOAL>x ≠ ↑m
<VAR>x : ℝ<VAR>h : Irrational x<GOAL>x ≠ 0
<VAR>x : ℝ<VAR>h : Irrational x<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>x ≠ OfNat.ofNat n
<VAR>q : ℚ<GOAL>¬Irrational ↑q
<VAR>m : ℤ<GOAL>¬Irrational ↑m
<VAR>m : ℕ<GOAL>¬Irrational ↑m
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>¬Irrational (OfNat.ofNat n)
<VAR>x y : ℝ<GOAL>Irrational (x + y) → Irrational x ∨ Irrational y
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (↑q + x)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational (↑q + x)
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (x + ↑q) → Irrational x
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational (x + ↑q)
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m + x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (x + ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (↑m + x)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (x + ↑m)
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (↑m + x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (x + ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<GOAL>Irrational (↑m + x)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<GOAL>Irrational (x + ↑m)
<VAR>x : ℝ<VAR>h : Irrational (-x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational (-x)
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational (x - ↑q)
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational (↑q - x)
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (x - ↑q)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (↑q - x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (x - ↑m)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (↑m - x)
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (x - ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m - x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<GOAL>Irrational (x - ↑m)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<GOAL>Irrational (↑m - x)
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (x - ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (↑m - x)<GOAL>Irrational x
<VAR>x y : ℝ<GOAL>Irrational (x * y) → Irrational x ∨ Irrational y
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (x * ↑q)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (x * ↑q)
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (↑q * x) → Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (↑q * x)
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (x * ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m * x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x * ↑m)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (↑m * x)
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (x * ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (↑m * x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>Irrational (x * ↑m)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>Irrational (↑m * x)
<VAR>x : ℝ<VAR>h : Irrational x⁻¹<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<GOAL>Irrational x⁻¹
<VAR>x y : ℝ<VAR>h : Irrational (x / y)<GOAL>Irrational x ∨ Irrational y
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (↑q / x)<GOAL>Irrational x
<VAR>q : ℚ<VAR>x : ℝ<VAR>h : Irrational (x / ↑q)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (↑q / x)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>Irrational (x / ↑q)
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (↑m / x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℤ<VAR>h : Irrational (x / ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (↑m / x)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x / ↑m)
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (↑m / x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>m : ℕ<VAR>h : Irrational (x / ↑m)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>Irrational (↑m / x)
<VAR>x : ℝ<VAR>h : Irrational x<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>Irrational (x / ↑m)
<VAR>x : ℝ<VAR>h : Irrational (1 / x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>h : Irrational (x * x)<GOAL>Irrational x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Irrational (x ^ n) → Irrational x
<VAR>x : ℝ<VAR>m : ℤ<GOAL>Irrational (x ^ m) → Irrational x
<VAR>x : ℝ<VAR>p : Polynomial ℤ<VAR>hx : Irrational x<VAR>p_nonzero : p ≠ 0<VAR>x_is_root : (Polynomial.aeval x) p = 0<GOAL>1 < p.natDegree
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (↑q + x) ↔ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (↑m + x) ↔ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑n + x) ↔ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (x + ↑q) ↔ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (x + ↑m) ↔ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x + ↑n) ↔ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (↑q - x) ↔ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (↑m - x) ↔ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑n - x) ↔ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (x - ↑q) ↔ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (x - ↑m) ↔ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x - ↑n) ↔ Irrational x
<VAR>x : ℝ<GOAL>Irrational (-x) ↔ Irrational x
<VAR>x : ℝ<GOAL>Irrational x⁻¹ ↔ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (↑q * x) ↔ q ≠ 0 ∧ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (↑m * x) ↔ m ≠ 0 ∧ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x
<VAR>n : ℕ<VAR>x : ℝ<GOAL>Irrational (x * ↑n) ↔ n ≠ 0 ∧ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (↑q / x) ↔ q ≠ 0 ∧ Irrational x
<VAR>q : ℚ<VAR>x : ℝ<GOAL>Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x
<VAR>m : ℤ<VAR>x : ℝ<GOAL>Irrational (↑m / x) ↔ m ≠ 0 ∧ Irrational x