emultiplicity_le_emultiplicity_of_dvd_right

English

If b ∣ c, then emultiplicity a b ≤ emultiplicity a c.

Русский

Если b делится на c, то эмплиплотность a в b не больше эмплиплотности a в c.

LaTeX

$$$ b \mid c \Rightarrow \operatorname{emultiplicity}(a,b) \le \operatorname{emultiplicity}(a,c) $$$

Lean4

theorem emultiplicity_le_emultiplicity_of_dvd_right {a b c : α} (h : b ∣ c) : emultiplicity a b ≤ emultiplicity a c :=
  emultiplicity_le_emultiplicity_iff.2 fun _ hb => hb.trans h

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