English
Let a, p be as above. If a ≠ 0, p is irreducible, and p divides a in the usual sense, then the associate of p occurs in the prime factorization of a, i.e., the element (Associates.mk p) lies in factors'(a).
Русский
Пусть a и p удовлетворяют условиям: a ≠ 0, p неприводимо, и p делит a. Тогда ассоциированное представление p встречается в разложении a, т.е. (Associates.mk p) входит в factors'(a).
LaTeX
$$$$a \\neq 0 \\;\wedge\\; \\mathrm{Irreducible}(p) \\;\wedge\\; p \\mid a \\;\\Rightarrow\\; \\mathrm{Subtype.mk}(\\mathrm{Associates.mk}(p), \\mathrm{irreducible\\_mk}.2\\,hp) \\in \\mathrm{factors'}\\,a.$$$$
Lean4
theorem mem_factors'_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :
Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a :=
by
obtain ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd ha0 hp hd
apply Multiset.mem_pmap.mpr; use q; use hq
exact Subtype.eq (Eq.symm (mk_eq_mk_iff_associated.mpr hpq))
