Documentation

Mathlib.Algebra.GroupWithZero.Semiconj

Lemmas about semiconjugate elements in a GroupWithZero. #

@[simp]
theorem SemiconjBy.zero_right {G₀ : Type u_1} [MulZeroClass G₀] (a : G₀) :
@[simp]
theorem SemiconjBy.zero_left {G₀ : Type u_1} [MulZeroClass G₀] (x : G₀) (y : G₀) :
@[simp]
theorem SemiconjBy.inv_symm_left_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} :
theorem SemiconjBy.inv_symm_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) :
theorem SemiconjBy.inv_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) :
@[simp]
theorem SemiconjBy.inv_right_iff₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} :
theorem SemiconjBy.div_right {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} {x' : G₀} {y' : G₀} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
SemiconjBy a (x / x') (y / y')
theorem SemiconjBy.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) (m : ) :
SemiconjBy a (x ^ m) (y ^ m)
theorem Commute.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ) :
Commute a (b ^ m)
theorem Commute.zpow_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ) :
Commute (a ^ m) b
theorem Commute.zpow_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ) (n : ) :
Commute (a ^ m) (b ^ n)
theorem Commute.zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ) :
Commute (a ^ n) a
theorem Commute.self_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ) :
Commute a (a ^ n)
theorem Commute.zpow_zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (m : ) (n : ) :
Commute (a ^ m) (a ^ n)