Mapping divisibility across multiplication-preserving homomorphisms

Main definitions

• map_dvd

Tags

divisibility, divides

theorem map_dvd {M : Type u_1} {N : Type u_2} [Semigroup M] [Semigroup N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (f : F) {a b : M} : a ∣ b → f a ∣ f b

theorem MulHom.map_dvd {M : Type u_1} {N : Type u_2} [Semigroup M] [Semigroup N] (f : M →ₙ* N) {a b : M} : a ∣ b → f a ∣ f b

theorem MonoidHom.map_dvd {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (f : M →* N) {a b : M} : a ∣ b → f a ∣ f b