# Documentation

## Mathlib.Algebra.Group.Commute.Basic

theorem AddCommute.neg_neg {G : Type u_1} {a : G} {b : G} :
theorem Commute.inv_inv {G : Type u_1} [] {a : G} {b : G} :
Commute a b
@[simp]
theorem AddCommute.neg_neg_iff {G : Type u_1} {a : G} {b : G} :
@[simp]
theorem Commute.inv_inv_iff {G : Type u_1} [] {a : G} {b : G} :
theorem AddCommute.sub_add_sub_comm {G : Type u_1} {a : G} {b : G} {c : G} {d : G} (hbd : ) (hbc : AddCommute (-b) c) :
a - b + (c - d) = a + c - (b + d)
theorem Commute.div_mul_div_comm {G : Type u_1} [] {a : G} {b : G} {c : G} {d : G} (hbd : Commute b d) (hbc : ) :
a / b * (c / d) = a * c / (b * d)
theorem AddCommute.add_sub_add_comm {G : Type u_1} {a : G} {b : G} {c : G} {d : G} (hcd : ) (hbc : AddCommute b (-c)) :
a + b - (c + d) = a - c + (b - d)
theorem Commute.mul_div_mul_comm {G : Type u_1} [] {a : G} {b : G} {c : G} {d : G} (hcd : Commute c d) (hbc : ) :
a * b / (c * d) = a / c * (b / d)
theorem AddCommute.sub_sub_sub_comm {G : Type u_1} {a : G} {b : G} {c : G} {d : G} (hbc : ) (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} [] {a : G} {b : G} {c : G} {d : G} (hbc : Commute b c) (hbd : ) (hcd : ) :
a / b / (c / d) = a / c / (b / d)
@[simp]
theorem AddCommute.neg_left_iff {G : Type u_1} [] {a : G} {b : G} :
@[simp]
theorem Commute.inv_left_iff {G : Type u_1} [] {a : G} {b : G} :
theorem Commute.inv_left {G : Type u_1} [] {a : G} {b : G} :
Commute a b

Alias of the reverse direction of Commute.inv_left_iff.

theorem AddCommute.neg_left {G : Type u_1} [] {a : G} {b : G} :
@[simp]
theorem AddCommute.neg_right_iff {G : Type u_1} [] {a : G} {b : G} :
@[simp]
theorem Commute.inv_right_iff {G : Type u_1} [] {a : G} {b : G} :
theorem Commute.inv_right {G : Type u_1} [] {a : G} {b : G} :
Commute a b

Alias of the reverse direction of Commute.inv_right_iff.

theorem AddCommute.neg_right {G : Type u_1} [] {a : G} {b : G} :
theorem AddCommute.neg_add_cancel {G : Type u_1} [] {a : G} {b : G} (h : ) :
-a + b + a = b
theorem Commute.inv_mul_cancel {G : Type u_1} [] {a : G} {b : G} (h : Commute a b) :
a⁻¹ * b * a = b
theorem AddCommute.neg_add_cancel_assoc {G : Type u_1} [] {a : G} {b : G} (h : ) :
-a + (b + a) = b
theorem Commute.inv_mul_cancel_assoc {G : Type u_1} [] {a : G} {b : G} (h : Commute a b) :
a⁻¹ * (b * a) = b
@[simp]
theorem AddCommute.conj_iff {G : Type u_1} [] {a : G} {b : G} (h : G) :
AddCommute (h + a + -h) (h + b + -h)
@[simp]
theorem Commute.conj_iff {G : Type u_1} [] {a : G} {b : G} (h : G) :
Commute (h * a * h⁻¹) (h * b * h⁻¹) Commute a b
theorem AddCommute.conj {G : Type u_1} [] {a : G} {b : G} (comm : ) (h : G) :
AddCommute (h + a + -h) (h + b + -h)
theorem Commute.conj {G : Type u_1} [] {a : G} {b : G} (comm : Commute a b) (h : G) :
Commute (h * a * h⁻¹) (h * b * h⁻¹)
@[simp]
theorem AddCommute.zsmul_right {G : Type u_1} [] {a : G} {b : G} (h : ) (m : ) :
@[simp]
theorem Commute.zpow_right {G : Type u_1} [] {a : G} {b : G} (h : Commute a b) (m : ) :
Commute a (b ^ m)
@[simp]
theorem AddCommute.zsmul_left {G : Type u_1} [] {a : G} {b : G} (h : ) (m : ) :
@[simp]
theorem Commute.zpow_left {G : Type u_1} [] {a : G} {b : G} (h : Commute a b) (m : ) :
Commute (a ^ m) b
theorem AddCommute.zsmul_zsmul {G : Type u_1} [] {a : G} {b : G} (h : ) (m : ) (n : ) :
theorem Commute.zpow_zpow {G : Type u_1} [] {a : G} {b : G} (h : Commute a b) (m : ) (n : ) :
Commute (a ^ m) (b ^ n)
theorem AddCommute.self_zsmul {G : Type u_1} [] (a : G) (n : ) :
theorem Commute.self_zpow {G : Type u_1} [] (a : G) (n : ) :
Commute a (a ^ n)
theorem AddCommute.zsmul_self {G : Type u_1} [] (a : G) (n : ) :