α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ abs a = abs b ↔ abs a * abs a = abs b * abs b
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ abs a = abs b ↔ a * a = b * b
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
no goals
α : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ abs a = abs b ↔ abs a * abs a = abs b * abs b
exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm