primeFactors_mono — Mathlib

English

If m divides n and n ≠ 0, then primeFactors(m) is a subset of primeFactors(n).

Русский

Если m делит n и n ≠ 0, то primeFactors(m) ⊆ primeFactors(n).

LaTeX

$$$m \mid n \land n \neq 0 \Rightarrow \text{primeFactors}(m) \subseteq \text{primeFactors}(n)$$$

Lean4

theorem primeFactors_mono (hmn : m ∣ n) (hn : n ≠ 0) : primeFactors m ⊆ primeFactors n :=
  by
  simp only [subset_iff, mem_primeFactors, and_imp]
  exact fun p hp hpm _ ↦ ⟨hp, hpm.trans hmn, hn⟩

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