English
Suppose f is not a unit in R[X], and whenever f f̃ = k k̃ for some k, then k belongs to { f, −f, f̃, −f̃ }. If f and f̃ are coprime, then f is irreducible.
Русский
Пусть f не является единицей в R[X], и если f f̃ = k k̃ для некоторого k, то справедливо, что k принадлежит {f, −f, f̃, −f̃}. Если f и f̃ взаимно просты, то f неизразим.
LaTeX
$$$ \\neg \\mathrm{IsUnit}(f) \\land \\Big( \\forall k, \\ f f^{\\sim} = k k^{\\sim} \\Rightarrow k \\in \\{ f,-f,f^{\\sim},-f^{\\sim} \\} \\Big) \\land \\mathrm{IsRelPrime}(f,f^{\\sim}) \\Rightarrow \\mathrm{Irreducible}(f) $$$
Lean4
theorem irreducible_of_mirror (h1 : ¬IsUnit f)
(h2 : ∀ k, f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror)
(h3 : IsRelPrime f f.mirror) : Irreducible f := by
constructor
· exact h1
· intro g h fgh
let k := g * h.mirror
have key : f * f.mirror = k * k.mirror := by
rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h, mul_comm g.mirror,
mul_assoc, ← mul_assoc]
have g_dvd_f : g ∣ f := by
rw [fgh]
exact dvd_mul_right g h
have h_dvd_f : h ∣ f := by
rw [fgh]
exact dvd_mul_left h g
have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
have h_dvd_k_rev : h ∣ k.mirror := by
rw [mirror_mul_of_domain, mirror_mirror]
exact dvd_mul_left h g.mirror
have hk := h2 k key
rcases hk with (hk | hk | hk | hk)
· exact Or.inr (h3 h_dvd_f (by rwa [← hk]))
· exact Or.inr (h3 h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
· exact Or.inl (h3 g_dvd_f (by rwa [← hk]))
· exact Or.inl (h3 g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))
