English
For d ≠ 0 and d ≤ n, d divides n if and only if (n/d).factorization = n.factorization − d.factorization.
Русский
Для d ≠ 0 и d ≤ n: d | n тогда и только тогда, когда (n/d).factorization = n.factorization − d.factorization.
LaTeX
$$$$ d \neq 0 \wedge d \le n \Rightarrow d \mid n \iff (n/d).factorization = n.factorization - d.factorization. $$$$
Lean4
theorem dvd_iff_div_factorization_eq_tsub {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) :
d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization :=
by
refine ⟨factorization_div, ?_⟩
rcases eq_or_lt_of_le hdn with (rfl | hd_lt_n); · simp
have h1 : n / d ≠ 0 := by simp [*]
intro h
rw [dvd_iff_le_div_mul n d]
by_contra h2
obtain ⟨p, hp⟩ := exists_factorization_lt_of_lt (mul_ne_zero h1 hd) (not_le.mp h2)
rwa [factorization_mul h1 hd, add_apply, ← lt_tsub_iff_right, h, tsub_apply, lt_self_iff_false] at hp
