mem_factoredNumbers_of_dvd — Mathlib

English

If m ∈ factoredNumbers(s) and k divides m, then k ∈ factoredNumbers(s).

Русский

Если m ∈ factoredNumbers(s) и k делит m, то k ∈ factoredNumbers(s).

LaTeX

$$m ∈ \mathrm{factoredNumbers}(s) \wedge k \mid m \Rightarrow k ∈ \mathrm{factoredNumbers}(s)$$

Lean4

/-- A number that divides an `s`-factored number is itself `s`-factored. -/
theorem mem_factoredNumbers_of_dvd {s : Finset ℕ} {m k : ℕ} (h : m ∈ factoredNumbers s) (h' : k ∣ m) :
    k ∈ factoredNumbers s := by
  obtain ⟨h₁, h₂⟩ := h
  have hk := ne_zero_of_dvd_ne_zero h₁ h'
  refine ⟨hk, fun p hp ↦ h₂ p ?_⟩
  rw [mem_primeFactorsList <| by assumption] at hp ⊢
  exact ⟨hp.1, hp.2.trans h'⟩

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