English
If d divides n, then (n/d).factorization = n.factorization − d.factorization.
Русский
Если d делит n, то (n/d).factorization = n.factorization − d.factorization.
LaTeX
$$$$ d \mid n \Rightarrow (n/d).factorization = n.factorization - d.factorization. $$$$
Lean4
@[simp]
theorem factorization_div {d n : ℕ} (h : d ∣ n) : (n / d).factorization = n.factorization - d.factorization :=
by
rcases eq_or_ne d 0 with (rfl | hd); · simp [zero_dvd_iff.mp h]
rcases eq_or_ne n 0 with (rfl | hn); · simp [tsub_eq_zero_of_le]
apply add_left_injective d.factorization
simp only
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd, Nat.div_mul_cancel h]
