English
Let a ≠ 0 and hp irreducible. Then Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a iff p ∣ a.
Русский
Пусть a ≠ 0 и p неприводимо. Тогда Subtype.mk(Associates.mk p, irreducible_mk.2 hp) ∈ factors' a ⇔ p ∣ a.
LaTeX
$$$$a \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow \\mathrm{Subtype.mk}(\\mathrm{Associates.mk}p,\\n\\t\\mathrm{irreducible\\_mk}.2\\,hp) \\in \\mathrm{factors'}\\,a \\iff p \\mid a.$$$$
Lean4
theorem count_ne_zero_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a :=
by
nontriviality α
rw [← Associates.mk_le_mk_iff_dvd]
refine
⟨fun h => Associates.le_of_count_ne_zero (Associates.mk_ne_zero.mpr ha0) (Associates.irreducible_mk.mpr hp) h,
fun h => ?_⟩
rw [← pow_one (Associates.mk p),
Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero.mpr ha0) (Associates.irreducible_mk.mpr hp)] at h
exact (zero_lt_one.trans_le h).ne'
