English
Let α be a Cancel-Commutative Monoid with Zero that is a Unique Factorization Monoid. If a ≠ 0 and p ∈ Associates α is irreducible, and p appears among the factors of a (in the factorization of a in the Associates sense), then p divides a in Associates.
Русский
Пусть α — CancelCommMonoidWithZero и UniqueFactorizationMonoid. Пусть a ≠ 0 и p ∈ Associates α является неприводимым; если p встречается среди разложения a (в разложении a с точки зрения Associates), то p делит a в смысле Associates.
LaTeX
$$$$\\forall a \\in \\alpha, \\forall p \\in \\mathrm{Associates}(\\alpha),\\; \\mathrm{Irreducible}(p) \\;\\land\\; a \\neq 0 \\;\\land\\; \\mathrm{Subtype.mk}(p, \\mathrm{irreducible\\_mk}.2\\,hp) \\in \\mathrm{factors'}\\,a\\; \\Rightarrow\\; p \\mid \\mathrm{Associates.mk}\\,a.$$$$
Lean4
theorem dvd_of_mem_factors' {a : α} {p : Associates α} {hp : Irreducible p} {hz : a ≠ 0}
(h_mem : Subtype.mk p hp ∈ factors' a) : p ∣ Associates.mk a :=
by
haveI := Classical.decEq (Associates α)
apply dvd_of_mem_factors
rw [factors_mk _ hz]
apply mem_factorSet_some.2 h_mem
