English
Let a ≠ 0 and p irreducible. Then the associated class of p occurs in the strict factorization of a if and only if p divides a in Associates.
Русский
Пусть a ≠ 0 и p неприводимо. Тогда ассоциированное представление p встречается в разложении a тогда и только тогда, когда p делит a в смысле Associates.
LaTeX
$$$$a \\neq 0 \\;\\land\\; \\mathrm{Irreducible}(p) \\;\\Longleftrightarrow\\; \\mathrm{Subtype.mk}(\\mathrm{Associates.mk}(p), \\mathrm{irreducible\\_mk}.2\\,hp) \\in \\mathrm{factors}\\, (\\mathrm{Associates.mk}\\,a) \\;\\Longleftrightarrow\\; p \\mid a.$$$$
Lean4
theorem mem_factors'_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a ↔ p ∣ a :=
by
constructor
· rw [← mk_dvd_mk]
apply dvd_of_mem_factors'
apply ha0
· apply mem_factors'_of_dvd ha0 hp
