English
A unit trinomial is irreducible if it has no common complex root with its mirror.
Русский
Единичный трином ирредуцируем, если у него нет общей нулевой точки с зеркалом этого полинома в комплексных числах.
LaTeX
$$Irreducible(p) if IsUnitTrinomial(p) and ∀ z ∈ ℂ, ¬(p(z)=0 ∧ p.mirror(z)=0).$$
Lean4
/-- A unit trinomial is irreducible if it has no complex roots in common with its mirror. -/
theorem irreducible_of_coprime' (hp : IsUnitTrinomial p) (h : ∀ z : ℂ, ¬(aeval z p = 0 ∧ aeval z (mirror p) = 0)) :
Irreducible p := by
refine hp.irreducible_of_coprime fun q hq hq' => ?_
suffices ¬0 < q.natDegree by
rcases hq with ⟨p, rfl⟩
replace hp := hp.leadingCoeff_isUnit
rw [leadingCoeff_mul] at hp
replace hp := isUnit_of_mul_isUnit_left hp
rw [not_lt, Nat.le_zero] at this
rwa [eq_C_of_natDegree_eq_zero this, isUnit_C, ← this]
intro hq''
rw [natDegree_pos_iff_degree_pos] at hq''
rw [← degree_map_eq_of_injective (algebraMap ℤ ℂ).injective_int] at hq''
obtain ⟨z, hz⟩ := Complex.exists_root hq''
rw [IsRoot, eval_map, ← aeval_def] at hz
refine h z ⟨?_, ?_⟩
· obtain ⟨g', hg'⟩ := hq
rw [hg', aeval_mul, hz, zero_mul]
· obtain ⟨g', hg'⟩ := hq'
rw [hg', aeval_mul, hz, zero_mul]
