English
Inequality of prime multisets corresponds to divisibility in ℕ+: factorMultiset m ≤ factorMultiset n iff m ∣ n.
Русский
Неравенство мультимножества простых соответствует делимости в ℕ+: factorMultiset m ≤ factorMultiset n iff m ∣ n.
LaTeX
$$$ m, n \\in \\mathbb{N}_{+}:\\ factorMultiset(m) \\le factorMultiset(n) \\iff m \\mid n $$$
Lean4
/-- We now have four different results that all encode the
idea that inequality of multisets corresponds to divisibility
of positive integers. -/
theorem factorMultiset_le_iff {m n : ℕ+} : factorMultiset m ≤ factorMultiset n ↔ m ∣ n :=
by
constructor
· intro h
rw [← prod_factorMultiset m, ← prod_factorMultiset m]
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h, prod_factorMultiset]
· intro h
rw [← mul_div_exact h, factorMultiset_mul]
exact le_self_add
