Theorem: sq_add_sq_eq_zero (LeanCourse/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0
Tactic:
sorry
State after:
no goals