Refactor of Algebra/Order/LatticeGroup with Algebra/Order/Group/Abs #6376
Description
The additive forms of several results in Algebra/Order/LatticeGroup have corresponding results in Algebra/Order/Group/Abs. E.g. compare the additive forms of the following results from Algebra/Order/LatticeGroup:
theorem le_mabs (a : α) : a ≤ |a| := sorry
theorem inv_le_abs (a : α) : a⁻¹ ≤ |a| := sorry
theorem one_le_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : 1 ≤ |a| := sorry
theorem mabs_mul_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |a * b| ≤ |a| * |b| := sorry
theorem mabs_mabs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |(|a|)| = |a| := sorry
theorem mabs_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : 1 ≤ a) : |a| = a := sorry
theorem abs_div_comm (a b : α) : |a / b| = |b / a| := sorry
theorem abs_abs_div_abs_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |(|a| / |b|)| ≤ |a / b| := sorry
theorem abs_inv (a : α) : |a⁻¹| = |a| := sorry
with these results from Algebra/Order/Group/Abs:
theorem le_abs_self (a : α) : a ≤ |a| := sorry
theorem neg_le_abs_self (a : α) : -a ≤ |a| := sorry
theorem abs_nonneg (a : α) : 0 ≤ |a| := sorry
theorem abs_add (a b : α) : |a + b| ≤ |a| + |b| := sorry
theorem abs_abs (a : α) : |(|a|)| = |a| := sorry
theorem abs_of_nonneg (h : 0 ≤ a) : |a| = a := sorry
theorem abs_sub_comm (a b : α) : |a - b| = |b - a| := sorry
theorem abs_abs_sub_abs_le_abs_sub (a b : α) : |(|a| - |b|)| ≤ |a - b| := sorry
theorem abs_neg (a : α) : |(-a)| = |a| := sorry
Would it make sense to refactor this?