# Mapping divisibility across multiplication-preserving homomorphisms #

## Main definitions #

- `map_dvd`

## Tags #

divisibility, divides

source
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
source
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
source
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