English
A unit trinomial p is irreducible if it is coprime with its mirror; more precisely, if hp : p.IsUnitTrinomial and h : IsCoprime p p.mirror, then Irreducible p.
Русский
Единичный триномиал p неприводим тогда, когда он взаимно прост с зеркальным образом p; то есть из hp : p.IsUnitTrinomial и h : IsCoprime p p.mirror следует Irreducible p.
LaTeX
$$$\\text{IsUnitTrinomial}(p) \\land IsCoprime(p, p.mirror) \\Rightarrow Irreducible(p)$$$
Lean4
theorem irreducible_of_coprime (hp : p.IsUnitTrinomial) (h : IsRelPrime p p.mirror) : Irreducible p :=
by
refine irreducible_of_mirror hp.not_isUnit (fun q hpq => ?_) h
have hq : IsUnitTrinomial q := (isUnitTrinomial_iff'' hpq).mp hp
obtain ⟨k, m, n, hkm, hmn, u, v, w, hp⟩ := hp
obtain ⟨k', m', n', hkm', hmn', x, y, z, hq⟩ := hq
have hk : k = k' := by
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natTrailingDegree hkm hmn u.ne_zero, ← hp, ←
natTrailingDegree_mul_mirror, hpq, natTrailingDegree_mul_mirror, hq,
trinomial_natTrailingDegree hkm' hmn' x.ne_zero]
have hn : n = n' := by
rw [← mul_right_inj' (show 2 ≠ 0 from two_ne_zero), ← trinomial_natDegree hkm hmn w.ne_zero, ← hp, ←
natDegree_mul_mirror, hpq, natDegree_mul_mirror, hq, trinomial_natDegree hkm' hmn' z.ne_zero]
subst hk
subst hn
rcases eq_or_eq_neg_of_sq_eq_sq (y : ℤ) (v : ℤ) ((Int.isUnit_sq y.isUnit).trans (Int.isUnit_sq v.isUnit).symm) with
(h1 | h1)
· rw [h1] at hq
rcases irreducible_aux3 hkm hmn hkm' hmn' u v w x z hp hq hpq with (h2 | h2)
· exact Or.inl h2
· exact Or.inr (Or.inr (Or.inl h2))
· rw [h1] at hq
rw [trinomial_def] at hp
rw [← neg_inj, neg_add, neg_add, ← neg_mul, ← neg_mul, ← neg_mul, ← C_neg, ← C_neg, ← C_neg] at hp
rw [← neg_mul_neg, ← mirror_neg] at hpq
rcases irreducible_aux3 hkm hmn hkm' hmn' (-u) (-v) (-w) x z hp hq hpq with (rfl | rfl)
· exact Or.inr (Or.inl rfl)
· exact Or.inr (Or.inr (Or.inr p.mirror_neg))
