Multiplicative homomorphisms respect semiconjugation and commutation. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, simp]
theorem
add_semiconj_by.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[has_add M]
[has_add N]
{a x y : M}
[add_hom_class F M N]
(h : add_semiconj_by a x y)
(f : F) :
add_semiconj_by (⇑f a) (⇑f x) (⇑f y)
@[protected, simp]
theorem
semiconj_by.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[has_mul M]
[has_mul N]
{a x y : M}
[mul_hom_class F M N]
(h : semiconj_by a x y)
(f : F) :
semiconj_by (⇑f a) (⇑f x) (⇑f y)
@[protected, simp]
theorem
add_commute.map
{F : Type u_1}
{M : Type u_2}
{N : Type u_3}
[has_add M]
[has_add N]
{x y : M}
[add_hom_class F M N]
(h : add_commute x y)
(f : F) :
add_commute (⇑f x) (⇑f y)