English
The right factorization divides b, i.e., factorizationLCMRight(a,b) | b.
Русский
Правая факторизация делит b.
LaTeX
$$$\text{factorizationLCMRight}(a,b) \mid b.$$$
Lean4
theorem factorizationLCMRight_dvd_right : factorizationLCMRight a b ∣ b :=
by
rcases eq_or_ne a 0 with rfl | ha
· simp [factorizationLCMRight]
rcases eq_or_ne b 0 with rfl | hb
· simp only [dvd_zero]
nth_rewrite 2 [← factorization_prod_pow_eq_self hb]
rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
· apply Finset.prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
· apply one_dvd
· rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le (not_le.1 le).le le_rfl
· intro p hp; rw [mem_support_iff] at hp ⊢
rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inr <| Nat.pos_of_ne_zero hp).ne'
· intros; rw [pow_zero]
