mathlib3 documentation

algebra.group_with_zero.semiconj

Lemmas about semiconjugate elements in a group_with_zero. #

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

@[simp]
theorem semiconj_by.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
@[simp]
theorem semiconj_by.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (x y : G₀) :
@[simp]
theorem semiconj_by.inv_symm_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
theorem semiconj_by.inv_symm_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
theorem semiconj_by.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
@[simp]
theorem semiconj_by.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
theorem semiconj_by.div_right {G₀ : Type u_3} [group_with_zero G₀] {a x y x' y' : G₀} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x / x') (y / y')