English
If p and q are trinomial polynomials related by p = trinomial k m n (...) and q = trinomial k m' n (...) and p*p.mirror = q*q.mirror, then q is either p or p.mirror.
Русский
Если p и q — триномиалы с указанной формой и p*p.mirror = q*q.mirror, то q равен либо p, либо p.mirror.
LaTeX
$$$q = p \\lor q = p.mirror$$$
Lean4
theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) (u v w : Units ℤ)
(hp : p = trinomial k m n (u : ℤ) v w) (hq : q = trinomial k m' n (u : ℤ) v w) (h : p * p.mirror = q * q.mirror) :
q = p ∨ q = p.mirror :=
by
let f : ℤ[X] → ℤ[X] := fun p => ⟨Finsupp.filter (· ∈ Set.Ioo (k + n) (n + n)) p.toFinsupp⟩
replace h := congr_arg f h
replace h := (irreducible_aux1 hkm hmn u v w hp).trans h
replace h := h.trans (irreducible_aux1 hkm' hmn' u v w hq).symm
rw [(isUnit_C.mpr v.isUnit).mul_right_inj] at h
rw [binomial_eq_binomial u.ne_zero w.ne_zero] at h
simp only [add_left_inj, Units.val_inj] at h
rcases h with (⟨rfl, -⟩ | ⟨rfl, rfl, h⟩ | ⟨-, hm, hm'⟩)
· exact Or.inl (hq.trans hp.symm)
· refine Or.inr ?_
rw [← trinomial_mirror hkm' hmn' u.ne_zero u.ne_zero, eq_comm, mirror_eq_iff] at hp
exact hq.trans hp
· grind
