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