OAI/AlgebraicGeometry/PlaneCurves/LineIntersections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Nagata.Workers.W14.polynomial_zero_of_three_roots line 16
2. theorem OAI.Nagata.Workers.W14.polynomial_zero_of_two_roots line 22
3. theorem OAI.Nagata.Workers.W14.polynomial_zero_of_double_zero_and_root line 33
4. def OAI.Nagata.Workers.W14.binaryAtOne line 63
5. theorem OAI.Nagata.Workers.W14.binaryAtOne_eq_sum line 66
6. theorem OAI.Nagata.Workers.W14.binaryAtOne_eval line 74
7. theorem OAI.Nagata.Workers.W14.binaryAtOne_natDegree_le line 78
8. theorem OAI.Nagata.Workers.W14.binaryAtOne_coeff_degree line 90
9. theorem OAI.Nagata.Workers.W14.binaryAtOne_eq_zero_imp line 108
10. theorem OAI.Nagata.Workers.W14.binaryAtOne_normalized_zero line 126
11. theorem OAI.Nagata.Workers.W14.binaryAtOne_derivative line 135
12. theorem OAI.Nagata.Workers.W14.binary_zero_of_three_projective_roots line 144
13. theorem OAI.Nagata.Workers.W14.binary_cubic_zero_of_singular_and_three_roots line 157
14. theorem OAI.Nagata.Workers.W14.homogeneous_line_dvd_of_three_projective_zeros line 184

    Source documentation

    A degree-at-most-two homogeneous equation vanishing at three distinct points on an actual projective line contains that line as a polynomial factor.

    theorem homogeneous_line_dvd_of_three_projective_zeros
        (L Q : MvPolynomial (Fin 3) ℂ) {d : ℕ}
        (hL : L.IsHomogeneous 1) (hne : L ≠ 0) (hQ : Q.IsHomogeneous d) (hd : d ≤ 2)
        (p : Fin 3 → PlanePoint) (hinj : Function.Injective p)
        (hLzero : ∀ i, MvPolynomial.eval (p i).rep L = 0)
        (hQzero : ∀ i, MvPolynomial.eval (p i).rep Q = 0) : L ∣ Q := by
    …

15. theorem OAI.Nagata.Workers.W14.homogeneous_line_dvd_cubic_of_singular_three_projective_zeros line 225