Additional lemmas about commuting pairs of elements in monoids

theorem AddCommute.neg_neg {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} : AddCommute a b → AddCommute (-a) (-b)

theorem Commute.inv_inv {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} : Commute a b → Commute a⁻¹ b⁻¹

@[simp]

theorem AddCommute.neg_neg_iff {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} : AddCommute (-a) (-b) ↔ AddCommute a b

@[simp]

theorem Commute.inv_inv_iff {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} : Commute a⁻¹ b⁻¹ ↔ Commute a b

theorem AddCommute.sub_add_sub_comm {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbd : AddCommute b d) (hbc : AddCommute (-b) c) : a - b + (c - d) = a + c - (b + d)

theorem Commute.div_mul_div_comm {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbd : Commute b d) (hbc : Commute b⁻¹ c) : a / b * (c / d) = a * c / (b * d)

theorem AddCommute.add_sub_add_comm {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hcd : AddCommute c d) (hbc : AddCommute b (-c)) : a + b - (c + d) = a - c + (b - d)

theorem Commute.mul_div_mul_comm {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hcd : Commute c d) (hbc : Commute b c⁻¹) : a * b / (c * d) = a / c * (b / d)

theorem AddCommute.sub_sub_sub_comm {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbc : AddCommute b c) (hbd : AddCommute (-b) d) (hcd : AddCommute (-c) d) : a - b - (c - d) = a - c - (b - d)

theorem Commute.div_div_div_comm {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} {c : G} {d : G} (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) : a / b / (c / d) = a / c / (b / d)