multiplicity_lt_of_emultiplicity_lt

English

Let a and b be elements of a monoid. If the emultiplicity of a with respect to b is less than n, then the multiplicity of a with respect to b is also less than n.

Русский

Пусть a и b — элементы моноида. Если эмплитичность a относительно b меньше n, то кратность a относительно b тоже меньше n.

LaTeX

$$$$\forall {\alpha} [Monoid \alpha] \; \{a,b: \alpha\} \; {n: \mathbb{N}},\; emultiplicity\ a\ b < n \rightarrow multiplicity\ a\ b < n.$$$$

Lean4

theorem multiplicity_lt_of_emultiplicity_lt {n : ℕ} (h : emultiplicity a b < n) : multiplicity a b < n := by
  exact_mod_cast multiplicity_le_emultiplicity.trans_lt h

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