English
If a, b ≠ 0 and the infimum of the principal associates of a and b is not 1, then there exists a prime p that divides both a and b.
Русский
Если a ≠ 0, b ≠ 0 и не существует меньшего делителя, чем единица, разделяющего оба, то существует простое p, делящее и a, и b.
LaTeX
$$$$a \\neq 0 \\land b \\neq 0 \\land (\\mathrm{Associates.mk}a \\sqcap \\mathrm{Associates.mk}b \\neq 1) \\Rightarrow \\exists p, \\mathrm{Prime}(p) \\land p \\mid a \\land p \\mid b.$$$$
Lean4
theorem exists_prime_dvd_of_not_inf_one {a b : α} (ha : a ≠ 0) (hb : b ≠ 0)
(h : Associates.mk a ⊓ Associates.mk b ≠ 1) : ∃ p : α, Prime p ∧ p ∣ a ∧ p ∣ b :=
by
have hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0 :=
by
contrapose! h with hf
change (factors (Associates.mk a) ⊓ factors (Associates.mk b)).prod = 1
rw [hf]
exact Multiset.prod_zero
rw [factors_mk a ha, factors_mk b hb, ← WithTop.coe_inf] at hz
obtain ⟨⟨p0, p0_irr⟩, p0_mem⟩ := Multiset.exists_mem_of_ne_zero ((mt WithTop.coe_eq_coe.mpr) hz)
rw [Multiset.inf_eq_inter] at p0_mem
obtain ⟨p, rfl⟩ : ∃ p, Associates.mk p = p0 := Quot.exists_rep p0
refine ⟨p, ?_, ?_, ?_⟩
· rw [← UniqueFactorizationMonoid.irreducible_iff_prime, ← irreducible_mk]
exact p0_irr
· apply dvd_of_mk_le_mk
apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left
apply ha
· apply dvd_of_mk_le_mk
apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).right
apply hb
