map_dvd — Mathlib

English

If f is a multiplicative map between semigroups and a ∣ b, then f(a) ∣ f(b).

Русский

Если f — мультипликативное отображение между полугруппами и a ∣ b, тогда f(a) ∣ f(b).

LaTeX

$$$ a \mid b \rightarrow f\,a \mid f\,b $$$

Lean4

@[gcongr]
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⟩

Похожие утверждения