mul_mem_smoothNumbers — Mathlib

English

The product of two n-smooth numbers is n-smooth.

Русский

Произведение двух n-гладких чисел снова гладкое.

LaTeX

$$$m_1 \in n.\mathrm{smoothNumbers} \land m_2 \in n.\mathrm{smoothNumbers} \Rightarrow m_1 m_2 \in n.\mathrm{smoothNumbers}$$$

Lean4

/-- The product of two `n`-smooth numbers is an `n`-smooth number. -/
theorem mul_mem_smoothNumbers {m₁ m₂ n : ℕ} (hm1 : m₁ ∈ n.smoothNumbers) (hm2 : m₂ ∈ n.smoothNumbers) :
    m₁ * m₂ ∈ n.smoothNumbers := by
  rw [smoothNumbers_eq_factoredNumbers] at hm1 hm2 ⊢
  exact mul_mem_factoredNumbers hm1 hm2

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