α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a b : α
⊢ a / b ⊔ (a / b)⁻¹ = b / a ⊔ (b / a)⁻¹
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a b : α
⊢ abs (a / b) = abs (b / a)
dsimp only [Abs.abs]
no goals
α : Type u
inst✝¹ : Lattice α
inst✝ : CommGroup α
a b : α
⊢ a / b ⊔ (a / b)⁻¹ = b / a ⊔ (b / a)⁻¹
rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]