mem_smoothNumbers_of_dvd — Mathlib

English

If m is n-smooth and k divides m, then k is n-smooth as well.

Русский

Если m является n-гладким, и k делит m, то k также является n-гладким.

LaTeX

$$$m \in \mathrm{smoothNumbers}(n) \land k \mid m \Rightarrow k \in \mathrm{smoothNumbers}(n)$$$

Lean4

/-- A number that divides an `n`-smooth number is itself `n`-smooth. -/
theorem mem_smoothNumbers_of_dvd {n m k : ℕ} (h : m ∈ smoothNumbers n) (h' : k ∣ m) : k ∈ smoothNumbers n :=
  by
  simp only [smoothNumbers_eq_factoredNumbers] at h ⊢
  exact mem_factoredNumbers_of_dvd h h'

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