factorization_le_factorization_mul_left

English

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

Русский

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

LaTeX

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

Lean4

theorem factorization_le_factorization_mul_left {a b : ℕ} (hb : b ≠ 0) : a.factorization ≤ (a * b).factorization :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp
  rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
  exact Dvd.intro b rfl

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