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)
@[simp]
theorem
AddCommute.neg_neg_iff
{G : Type u_1}
[SubtractionMonoid G]
{a : G}
{b : G}
:
AddCommute (-a) (-b) ↔ AddCommute a b
@[simp]
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)
:
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))
:
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)
: