Lemmas about commuting elements in a MonoidWithZero or a GroupWithZero.

theorem Ring.mul_inverse_rev' {M₀ : Type u_1} [MonoidWithZero M₀] {a b : M₀} (h : Commute a b) : inverse (a * b) = inverse b * inverse a

theorem Ring.mul_inverse_rev {M₀ : Type u_3} [CommMonoidWithZero M₀] (a b : M₀) : inverse (a * b) = inverse b * inverse a

theorem Ring.inverse_pow {M₀ : Type u_1} [MonoidWithZero M₀] (r : M₀) (n : ℕ) : inverse r ^ n = inverse (r ^ n)

theorem Ring.inverse_pow_mul_eq_iff_eq_mul {M₀ : Type u_1} [MonoidWithZero M₀] {a : M₀} (b c : M₀) (ha : IsUnit a) {k : ℕ} : inverse a ^ k * b = c ↔ b = a ^ k * c

theorem Commute.ringInverse_ringInverse {M₀ : Type u_1} [MonoidWithZero M₀] {a b : M₀} (h : Commute a b) : Commute (Ring.inverse a) (Ring.inverse b)

@[simp]

theorem Commute.zero_right {G₀ : Type u_2} [MulZeroClass G₀] (a : G₀) : Commute a 0

@[simp]

theorem Commute.zero_left {G₀ : Type u_2} [MulZeroClass G₀] (a : G₀) : Commute 0 a

@[simp]

theorem Commute.inv_left_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] {a b : G₀} : Commute a⁻¹ b ↔ Commute a b

theorem Commute.inv_left₀ {G₀ : Type u_2} [GroupWithZero G₀] {a b : G₀} (h : Commute a b) : Commute a⁻¹ b

theorem Commute.inv_left_self₀ {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : Commute a⁻¹ a

@[simp]

theorem Commute.inv_right_iff₀ {G₀ : Type u_2} [GroupWithZero G₀] {a b : G₀} : Commute a b⁻¹ ↔ Commute a b

theorem Commute.inv_right₀ {G₀ : Type u_2} [GroupWithZero G₀] {a b : G₀} (h : Commute a b) : Commute a b⁻¹

theorem Commute.inv_right_self₀ {G₀ : Type u_2} [GroupWithZero G₀] (a : G₀) : Commute a a⁻¹

@[simp]

theorem Commute.div_right {G₀ : Type u_2} [GroupWithZero G₀] {a b c : G₀} (hab : Commute a b) (hac : Commute a c) : Commute a (b / c)

@[simp]

theorem Commute.div_left {G₀ : Type u_2} [GroupWithZero G₀] {a b c : G₀} (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c

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