English
If W.Nonsingular P and W.Nonsingular Q then W.Nonsingular (W.add P Q).
Русский
Если W.Nonsingular P и W.Nonsingular Q, то W.Nonsingular (W.add P Q).
LaTeX
$$$ W.Nonsingular P \\rightarrow W.Nonsingular Q \\rightarrow 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_Y_of_Z_eq_zero hP hPz).pow 4,
nonsingular_zero]
·
simpa only [add_of_Z_eq_zero_left hP.left hPz hQz,
nonsingular_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).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_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg]
· by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
· by_cases hy : P y * Q z = Q y * P z
·
simp only [add_of_Y_eq hP.left 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 = Q x * P z
·
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 hQz 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 hP.left hQ.left hx]
