constructor
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0
case mp
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x ^ 2 + y ^ 2 = 0 → x = 0 ∧ y = 0

case mpr
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ x = 0 ∧ y = 0 → x ^ 2 + y ^ 2 = 0