feat(Algebra/Order/LatticeGroup): Add missing abs_inv to LatticeGro…

…up (#6357)

Adds missing `abs_inv` to LatticeGroup



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -189,6 +189,11 @@ theorem inv_le_abs (a : α) : a⁻¹ ≤ |a| :=
 #align lattice_ordered_comm_group.inv_le_abs LatticeOrderedCommGroup.inv_le_abs
 #align lattice_ordered_comm_group.neg_le_abs LatticeOrderedCommGroup.neg_le_abs
 
+@[to_additive (attr := simp)]
+theorem abs_inv (a : α) : |a⁻¹| = |a| := calc
+  |a⁻¹| = a⁻¹ ⊔ (a⁻¹)⁻¹ := rfl
+  _ = a ⊔ a⁻¹ := by rw [inv_inv, sup_comm]
+
 -- 0 ≤ a⁺
 @[to_additive pos_nonneg]
 theorem one_le_pos (a : α) : 1 ≤ a⁺ :=