structure EllipticCurveP2Data (C : Type u_1) (F : Type u_2) [Field F] : Type (max (max u_1 u_2) (u_3 + 1))

• curveInst : FunctionFieldCurve C F
• Line : Type u_3
• lineIntersectionDivisor : self.Line → CurveDivisor C
• linearFormRatio : self.Line → self.Line → Fˣ
• restrictLinearForm : self.Line → Fˣ
• ratio_eq_mul_inv (L₁ L₂ : self.Line) : self.linearFormRatio L₁ L₂ = self.restrictLinearForm L₁ * (self.restrictLinearForm L₂)⁻¹

noncomputable def EllipticCurveP2Data.pdiv {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (f : Fˣ) : CurveDivisor C

theorem EllipticCurveP2Data.bezout_degree {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (L : E.Line) : (CurveDivisor.degree C) (E.lineIntersectionDivisor L) = 3

theorem EllipticCurveP2Data.bezout_divisor {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (L : E.Line) : E.pdiv (E.restrictLinearForm L) = E.lineIntersectionDivisor L

theorem EllipticCurveP2Data.lineIntersectionDivisor_degree {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (L : E.Line) : (CurveDivisor.degree C) (E.lineIntersectionDivisor L) = 3

theorem EllipticCurveP2Data.div_restrictLinearForm {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (L : E.Line) : E.pdiv (E.restrictLinearForm L) = E.lineIntersectionDivisor L

theorem EllipticCurveP2Data.pdiv_mul {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (f g : Fˣ) : E.pdiv (f * g) = E.pdiv f + E.pdiv g

theorem EllipticCurveP2Data.pdiv_inv {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (f : Fˣ) : E.pdiv f⁻¹ = -E.pdiv f

theorem EllipticCurveP2Data.lemma_23_17 {C : Type u_1} {F : Type u_2} [Field F] (E : EllipticCurveP2Data C F) (L₁ L₂ : E.Line) : E.pdiv (E.linearFormRatio L₁ L₂) = E.lineIntersectionDivisor L₁ - E.lineIntersectionDivisor L₂