Mathlib.Algebra.Divisibility.Hom

Module docstring

{"# Mapping divisibility across multiplication-preserving homomorphisms

Main definitions

map_dvd

Tags

divisibility, divides "}

map_dvd theorem

[Semigroup M] [Semigroup N] {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F) {a b} : a ∣ b → f a ∣ f b

Full source

theorem map_dvd [Semigroup M] [Semigroup N] {F : Type*} [FunLike F M N] [MulHomClass F M N]
    (f : F) {a b} : a ∣ b → f a ∣ f b
  | ⟨c, h⟩ => ⟨f c, h.symm ▸ map_mul f a c⟩

Divisibility Preservation Under Multiplication-Preserving Homomorphisms

Informal description

Let $M$ and $N$ be semigroups, and let $F$ be a type of homomorphisms from $M$ to $N$ that preserve multiplication. For any homomorphism $f \colon M \to N$ in $F$ and any elements $a, b \in M$, if $a$ divides $b$ in $M$, then $f(a)$ divides $f(b)$ in $N$.

MulHom.map_dvd theorem

[Semigroup M] [Semigroup N] (f : M →ₙ* N) {a b} : a ∣ b → f a ∣ f b

Full source

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

Divisibility is preserved under multiplicative homomorphisms

Informal description

Let $M$ and $N$ be semigroups, and let $f \colon M \to N$ be a multiplicative homomorphism (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in M$). For any elements $a, b \in M$, if $a$ divides $b$ in $M$, then $f(a)$ divides $f(b)$ in $N$.

MonoidHom.map_dvd theorem

[Monoid M] [Monoid N] (f : M →* N) {a b} : a ∣ b → f a ∣ f b

Full source

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

Divisibility Preservation Under Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any elements $a, b \in M$, if $a$ divides $b$ in $M$, then $f(a)$ divides $f(b)$ in $N$.