mathlib3 documentation

algebra.group_with_zero.commute

Lemmas about commuting elements in a monoid_with_zero or a group_with_zero. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem ring.mul_inverse_rev' {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
theorem ring.mul_inverse_rev {M₀ : Type u_1} [comm_monoid_with_zero M₀] (a b : M₀) :
theorem commute.ring_inverse_ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
@[simp]
theorem commute.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
@[simp]
theorem commute.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
@[simp]
theorem commute.inv_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
theorem commute.inv_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : commute a b) :
@[simp]
theorem commute.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
theorem commute.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : commute a b) :
@[simp]
theorem commute.div_right {G₀ : Type u_3} [group_with_zero 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_3} [group_with_zero G₀] {a b c : G₀} (hac : commute a c) (hbc : commute b c) :
commute (a / b) c