le_emultiplicity_iff_replicate_subperm_primeFactorsList

English

For prime a and b ≠ 0, and any n, we have ↑n ≤ emultiplicity a b iff the list replicate n a is a sub-permutation of b’s primeFactorsList.

Русский

Для простого a и b ≠ 0 выполняется: ↑n ≤ emultiplicity a b эквивалентно тому, что список replicate n a является под-частью списка простых факторов b.

LaTeX

$$$\\\\uparrow n \\\\le \\\\operatorname{emultiplicity} a b \\\\Longleftrightarrow (\\\\text{replicate } n\,a) \\,<+~\\\\, b.\\\\primeFactorsList$$$

Lean4

theorem le_emultiplicity_iff_replicate_subperm_primeFactorsList {a b : ℕ} {n : ℕ} (ha : a.Prime) (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList :=
  (replicate_subperm_primeFactorsList_iff ha hb).trans pow_dvd_iff_le_emultiplicity |>.symm

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