Documentation

Mathlib.Algebra.Hom.Commute

Multiplicative homomorphisms respect semiconjugation and commutation. #

@[simp]
theorem AddSemiconjBy.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {a : M} {x : M} {y : M} [AddHomClass F M N] (h : AddSemiconjBy a x y) (f : F) :
AddSemiconjBy (f a) (f x) (f y)
@[simp]
theorem SemiconjBy.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {a : M} {x : M} {y : M} [MulHomClass F M N] (h : SemiconjBy a x y) (f : F) :
SemiconjBy (f a) (f x) (f y)
@[simp]
theorem AddCommute.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {x : M} {y : M} [AddHomClass F M N] (h : AddCommute x y) (f : F) :
AddCommute (f x) (f y)
@[simp]
theorem Commute.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {x : M} {y : M} [MulHomClass F M N] (h : Commute x y) (f : F) :
Commute (f x) (f y)
@[simp]
theorem AddSemiconjBy.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {a : M} {x : M} {y : M} [AddHomClass F M N] (f : F) (hf : Function.Injective f) (h : AddSemiconjBy (f a) (f x) (f y)) :
@[simp]
theorem SemiconjBy.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {a : M} {x : M} {y : M} [MulHomClass F M N] (f : F) (hf : Function.Injective f) (h : SemiconjBy (f a) (f x) (f y)) :
@[simp]
theorem AddCommute.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {x : M} {y : M} [AddHomClass F M N] {f : F} (hf : Function.Injective f) (h : AddCommute (f x) (f y)) :
@[simp]
theorem Commute.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {x : M} {y : M} [MulHomClass F M N] {f : F} (hf : Function.Injective f) (h : Commute (f x) (f y)) :