Multiplicative homomorphisms respect semiconjugation and commutation.

@[simp]

theorem SemiconjBy.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {a x y : M} [FunLike F M N] [MulHomClass F M N] (h : SemiconjBy a x y) (f : F) : SemiconjBy (f a) (f x) (f y)

@[simp]

theorem AddSemiconjBy.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {a x y : M} [FunLike F M N] [AddHomClass F M N] (h : AddSemiconjBy a x y) (f : F) : AddSemiconjBy (f a) (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 y : M} [FunLike F M N] [MulHomClass F M N] (h : Commute x y) (f : F) : Commute (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 y : M} [FunLike F M N] [AddHomClass F M N] (h : AddCommute x y) (f : F) : AddCommute (f x) (f y)

theorem SemiconjBy.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {a x y : M} [FunLike F M N] [MulHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (h : SemiconjBy (f a) (f x) (f y)) : SemiconjBy a x y

theorem AddSemiconjBy.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {a x y : M} [FunLike F M N] [AddHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (h : AddSemiconjBy (f a) (f x) (f y)) : AddSemiconjBy a x y

theorem Commute.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {x y : M} [FunLike F M N] [MulHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (h : Commute (f x) (f y)) : Commute x y

theorem AddCommute.of_map {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {x y : M} [FunLike F M N] [AddHomClass F M N] {f : F} (hf : Function.Injective ⇑f) (h : AddCommute (f x) (f y)) : AddCommute x y

theorem semiconjBy_map_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] {a : M} [FunLike F M N] [MulHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {x y : M} : SemiconjBy (f a) (f x) (f y) ↔ SemiconjBy a x y

theorem addSemiconjBy_map_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] {a : M} [FunLike F M N] [AddHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {x y : M} : AddSemiconjBy (f a) (f x) (f y) ↔ AddSemiconjBy a x y

theorem commute_map_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {x y : M} : Commute (f x) (f y) ↔ Commute x y

theorem addCommute_map_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] {f : F} (hf : Function.Injective ⇑f) {x y : M} : AddCommute (f x) (f y) ↔ AddCommute x y