mathlib3 documentation

algebra.hom.commute

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)
@[protected, simp]
theorem commute.map {F : Type u_1} {M : Type u_2} {N : Type u_3} [has_mul M] [has_mul N] {x y : M} [mul_hom_class F M N] (h : commute x y) (f : F) :
commute (f x) (f y)