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.

source
@[simp]
theorem semiconj_by.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
semiconj_by a 0 0
source
@[simp]
theorem semiconj_by.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (x y : G₀) :
semiconj_by 0 x y
source
@[simp]
theorem semiconj_by.inv_symm_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
semiconj_by a⁻¹ x y ↔ semiconj_by a y x
source
theorem semiconj_by.inv_symm_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
semiconj_by a⁻¹ y x
source
theorem semiconj_by.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
semiconj_by a x⁻¹ y⁻¹
source
@[simp]
theorem semiconj_by.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y
source
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')