Documentation

Mathlib.Algebra.GroupWithZero.Commute

Lemmas about commuting elements in a MonoidWithZero or a GroupWithZero. #

theorem Ring.mul_inverse_rev' {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {b : M₀} (h : Commute a b) :
theorem Ring.mul_inverse_rev {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] (a : M₀) (b : M₀) :
theorem Commute.ring_inverse_ring_inverse {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {b : M₀} (h : Commute a b) :
@[simp]
theorem Commute.zero_right {G₀ : Type u_1} [inst : MulZeroClass G₀] (a : G₀) :
@[simp]
theorem Commute.zero_left {G₀ : Type u_1} [inst : MulZeroClass G₀] (a : G₀) :
@[simp]
theorem Commute.inv_left_iff₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} :
theorem Commute.inv_left₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) :
@[simp]
theorem Commute.inv_right_iff₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} :
theorem Commute.inv_right₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) :
@[simp]
theorem Commute.div_right {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hab : Commute a b) (hac : Commute a c) :
Commute a (b / c)
@[simp]
theorem Commute.div_left {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {b : G₀} {c : G₀} (hac : Commute a c) (hbc : Commute b c) :
Commute (a / b) c