English
If P and Q are nonsingular points on W, then their sum W.add P Q is also nonsingular.
Русский
Если P и Q — несингулярные точки на W, то сумма W.add P Q также несингулярна.
LaTeX
$$$W.Nonsingular(P) \land W.Nonsingular(Q) \implies W.Nonsingular(W.add(P,Q))$$$
Lean4
theorem nonsingular_add {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : W.Nonsingular <| W.add P Q :=
by
by_cases hPz : P z = 0
· by_cases hQz : Q z = 0
·
simp only [add_of_Z_eq_zero hP hQ hPz hQz, nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2,
nonsingular_zero]
·
simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
nonsingular_smul _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]
· by_cases hQz : Q z = 0
·
simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
nonsingular_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]
· by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
· by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3
·
simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right,
nonsingular_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]
·
simp only [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
nonsingular_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, nonsingular_zero]
·
classical
have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
·
simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]
· simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx, nonsingular_smul _ <| isUnit_addZ_of_X_ne hx]
