English
If a is nonzero and p is irreducible and p divides a, then p is associated to some factor of a's factorization.
Русский
Если a ≠ 0 и p ирредуцируемый и p делит a, то p ассоциирован с некоторым фактором разложения a.
LaTeX
$$$\forall a,p,\; a\neq 0,\; \mathrm{Irreducible}(p)\; \wedge\; p \mid a \Rightarrow \exists q\in \mathrm{factors}(a),\; p \sim q.$$$
Lean4
theorem exists_mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ factors a, p ~ᵤ q :=
fun ⟨b, hb⟩ =>
have hb0 : b ≠ 0 := fun hb0 => by simp_all
have : Multiset.Rel Associated (p ::ₘ factors b) (factors a) :=
factors_unique (fun _ hx => (Multiset.mem_cons.1 hx).elim (fun h => h.symm ▸ hp) (irreducible_of_factor _))
irreducible_of_factor
(Associated.symm <|
calc
Multiset.prod (factors a) ~ᵤ a := factors_prod ha0
_ = p * b := hb
_ ~ᵤ Multiset.prod (p ::ₘ factors b) := by rw [Multiset.prod_cons]; exact (factors_prod hb0).symm.mul_left _)
Multiset.exists_mem_of_rel_of_mem this (by simp)
