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.

source
theorem ring.mul_inverse_rev' {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
ring.inverse (a * b) = ring.inverse b * ring.inverse a
source
theorem ring.mul_inverse_rev {M₀ : Type u_1} [comm_monoid_with_zero M₀] (a b : M₀) :
ring.inverse (a * b) = ring.inverse b * ring.inverse a
source
theorem commute.ring_inverse_ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
commute (ring.inverse a) (ring.inverse b)
source
@[simp]
theorem commute.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
commute a 0
source
@[simp]
theorem commute.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
commute 0 a
source
@[simp]
theorem commute.inv_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
commute a⁻¹ b ↔ commute a b
source
theorem commute.inv_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : commute a b) :
commute a⁻¹ b
source
@[simp]
theorem commute.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
commute a b⁻¹ ↔ commute a b
source
theorem commute.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : commute a b) :
commute a b⁻¹
source
@[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)
source
@[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