Theorems · Theorem · group theory

SemiconjBy.mul_right

∀ {S : Type u_1} [inst : Semigroup S] {a x y x' y' : S},
  SemiconjBy a x y → SemiconjBy a x' y' → SemiconjBy a (x * x') (y * y')

If a semiconjugates x to y and x' to y', then it semiconjugates x * x' to y * y'.

Defined in

Mathlib.Algebra.Group.Semiconj.Defs

Cited by

5 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Semigroup