Additional lemmas about commuting pairs of elements in monoids

theorem SemiconjBy.function_semiconj_mul_left {G : Type u_1} [Semigroup G] {a b c : G} (h : SemiconjBy a b c) : Function.Semiconj (fun (x : G) => a * x) (fun (x : G) => b * x) fun (x : G) => c * x

theorem AddSemiconjBy.function_semiconj_add_left {G : Type u_1} [AddSemigroup G] {a b c : G} (h : AddSemiconjBy a b c) : Function.Semiconj (fun (x : G) => a + x) (fun (x : G) => b + x) fun (x : G) => c + x

theorem Commute.function_commute_mul_left {G : Type u_1} [Semigroup G] {a b : G} (h : Commute a b) : Function.Commute (fun (x : G) => a * x) fun (x : G) => b * x

theorem AddCommute.function_commute_add_left {G : Type u_1} [AddSemigroup G] {a b : G} (h : AddCommute a b) : Function.Commute (fun (x : G) => a + x) fun (x : G) => b + x

theorem SemiconjBy.function_semiconj_mul_right_swap {G : Type u_1} [Semigroup G] {a b c : G} (h : SemiconjBy a b c) : Function.Semiconj (fun (x : G) => x * a) (fun (x : G) => x * c) fun (x : G) => x * b

theorem AddSemiconjBy.function_semiconj_add_right_swap {G : Type u_1} [AddSemigroup G] {a b c : G} (h : AddSemiconjBy a b c) : Function.Semiconj (fun (x : G) => x + a) (fun (x : G) => x + c) fun (x : G) => x + b

theorem Commute.function_commute_mul_right {G : Type u_1} [Semigroup G] {a b : G} (h : Commute a b) : Function.Commute (fun (x : G) => x * a) fun (x : G) => x * b

theorem AddCommute.function_commute_add_right {G : Type u_1} [AddSemigroup G] {a b : G} (h : AddCommute a b) : Function.Commute (fun (x : G) => x + a) fun (x : G) => x + b

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

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

@[simp]

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

@[simp]

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

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

theorem AddCommute.sub_add_sub_comm {G : Type u_1} [SubtractionMonoid G] {a b c d : G} (hbd : AddCommute b 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 b c d : G} (hcd : Commute c 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 b c d : G} (hcd : AddCommute c d) (hbc : AddCommute b (-c)) : a + b - (c + d) = a - c + (b - d)

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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Commute.inv_left_iff.

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

Alias of the reverse direction of AddCommute.neg_left_iff.

theorem Commute.inv_left_self {G : Type u_1} [Group G] (a : G) : Commute a⁻¹ a

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Commute.inv_right_iff.

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

Alias of the reverse direction of AddCommute.neg_right_iff.

theorem Commute.inv_right_self {G : Type u_1} [Group G] (a : G) : Commute a a⁻¹

theorem Commute.inv_mul_cancel {G : Type u_1} [Group G] {a b : G} (h : Commute a b) : a⁻¹ * b * a = b

theorem AddCommute.neg_add_cancel {G : Type u_1} [AddGroup G] {a b : G} (h : AddCommute a b) : -a + b + a = b

theorem Commute.inv_mul_cancel_assoc {G : Type u_1} [Group G] {a b : G} (h : Commute a b) : a⁻¹ * (b * a) = b

theorem AddCommute.neg_add_cancel_assoc {G : Type u_1} [AddGroup G] {a b : G} (h : AddCommute a b) : -a + (b + a) = b

@[simp]

theorem Commute.conj_iff {G : Type u_1} [Group G] {a b : G} (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b

@[simp]

theorem AddCommute.addConj_iff {G : Type u_1} [AddGroup G] {a b : G} (h : G) : AddCommute (h + a + -h) (h + b + -h) ↔ AddCommute a b

theorem Commute.conj {G : Type u_1} [Group G] {a b : G} (comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹)

theorem AddCommute.addConj {G : Type u_1} [AddGroup G] {a b : G} (comm : AddCommute a b) (h : G) : AddCommute (h + a + -h) (h + b + -h)

@[simp]

theorem Commute.zpow_right {G : Type u_1} [Group G] {a b : G} (h : Commute a b) (m : ℤ) : Commute a (b ^ m)

@[simp]

theorem AddCommute.zsmul_right {G : Type u_1} [AddGroup G] {a b : G} (h : AddCommute a b) (m : ℤ) : AddCommute a (m • b)

@[simp]

theorem Commute.zpow_left {G : Type u_1} [Group G] {a b : G} (h : Commute a b) (m : ℤ) : Commute (a ^ m) b

@[simp]

theorem AddCommute.zsmul_left {G : Type u_1} [AddGroup G] {a b : G} (h : AddCommute a b) (m : ℤ) : AddCommute (m • a) b

theorem Commute.zpow_zpow {G : Type u_1} [Group G] {a b : G} (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n)

theorem AddCommute.zsmul_zsmul {G : Type u_1} [AddGroup G] {a b : G} (h : AddCommute a b) (m n : ℤ) : AddCommute (m • a) (n • b)

theorem Commute.self_zpow {G : Type u_1} [Group G] (a : G) (n : ℤ) : Commute a (a ^ n)

theorem AddCommute.self_zsmul {G : Type u_1} [AddGroup G] (a : G) (n : ℤ) : AddCommute a (n • a)

theorem Commute.zpow_self {G : Type u_1} [Group G] (a : G) (n : ℤ) : Commute (a ^ n) a

theorem AddCommute.zsmul_self {G : Type u_1} [AddGroup G] (a : G) (n : ℤ) : AddCommute (n • a) a

theorem Commute.zpow_zpow_self {G : Type u_1} [Group G] (a : G) (m n : ℤ) : Commute (a ^ m) (a ^ n)

theorem AddCommute.zsmul_zsmul_self {G : Type u_1} [AddGroup G] (a : G) (m n : ℤ) : AddCommute (m • a) (n • a)

theorem pow_inv_comm {G : Type u_1} [Group G] (a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

theorem nsmul_neg_comm {G : Type u_1} [AddGroup G] (a : G) (m n : ℕ) : m • -a + n • a = n • a + m • -a