factorization_le_factorization_mul_right

English

If a ≠ 0, then b.factorization ≤ (a b).factorization; i.e., multiplying on the left does not decrease factorization coordinates.

Русский

Если a ≠ 0, то факторизация b ≤ факторизация (a b); то есть умножение слева не уменьшает показатель факторов.

LaTeX

$$$$ a \neq 0 \Rightarrow b\text{.factorization} \le (a b)\text{.factorization} \quad\text{for all primes } p.$$$$

Lean4

theorem factorization_le_factorization_mul_right {a b : ℕ} (ha : a ≠ 0) : b.factorization ≤ (a * b).factorization :=
  by
  rw [mul_comm]
  apply factorization_le_factorization_mul_left ha

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