Binary Tower Irreducibility and Trace #
Irreducibility and trace-map criteria for binary tower defining polynomials.
theorem
traceMapProperty_of_quadratic_extension
(F_prev : Type u_1)
[Field F_prev]
[Fintype F_prev]
(k : ℕ)
(fintypeCardPrev : Fintype.card F_prev = 2 ^ 2 ^ k)
(t1 : F_prev)
[instNeZero_t1 : NeZero t1]
{F_cur : Type u_2}
[Field F_cur]
(u : F_cur)
[instNeZero_u : NeZero u]
[Algebra F_prev F_cur]
(h_rel : SpecialElementRelation t1 u)
(prev_trace_map : TraceMapProperty F_prev t1 k)
(sumZeroIffEq : ∀ (x y : F_cur), x + y = 0 ↔ x = y)
:
TraceMapProperty F_cur u (k + 1)
Instance : The trace map property for a quadratic extension defined by a root u of X^2 + t1 * X + 1, assuming the trace property for t1 at the previous level.
theorem
not_irreducible_of_isRoot_of_degree_gt_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
(p : Polynomial R)
(h_root : ∃ (r : R), p.IsRoot r)
(h_deg : p.degree > 1)
:
A polynomial with a degree greater than 1 is not irreducible if it has a root in R.