Multiplicative homomorphisms respect semiconjugation and commutation. #
@[simp]
theorem
AddSemiconjBy.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[inst : Add M]
[inst : Add N]
{a : M}
{x : M}
{y : M}
[inst : 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}
[inst : Mul M]
[inst : Mul N]
{a : M}
{x : M}
{y : M}
[inst : 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}
[inst : Add M]
[inst : Add N]
{x : M}
{y : M}
[inst : AddHomClass F M N]
(h : AddCommute x y)
(f : F)
:
AddCommute (↑f x) (↑f y)