English
If α ∈ L satisfies α^{finrank(K,L)} = algebraMap_KL(a) and K⟮α⟯ = ⊤, then X^{finrank(K,L)} − C a is irreducible over K.
Русский
Если α ∈ L удовлетворяет α^{finrank(K,L)} = algebraMap_KL(a) и K⟮α⟯ = ⊤, то X^{finrank(K,L)} − C a ирродуцируем над K.
LaTeX
$$$\alpha^{\mathrm{finrank}(K,L)} = \mathrm{algebraMap}_{K,L}(a) \quad\text{и}\quad K⟮α⟯ = ⊤ \Rightarrow X^{\mathrm{finrank}(K,L)} - C a\ \text{ ирродовимо над } K.$$$
Lean4
theorem irreducible_X_pow_sub_C_of_root_adjoin_eq_top {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a)
(hα : K⟮α⟯ = ⊤) : Irreducible (X ^ (finrank K L) - C a) :=
by
have : X ^ (finrank K L) - C a = minpoly K α :=
by
refine minpoly.unique _ _ (monic_X_pow_sub_C _ finrank_pos.ne.symm) ?_ ?_
· simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]
· intro q hq hq'
refine le_trans ?_ (degree_le_of_dvd (minpoly.dvd _ _ hq') hq.ne_zero)
rw [degree_X_pow_sub_C finrank_pos, degree_eq_natDegree (minpoly.ne_zero (IsIntegral.of_finite K α)), ←
IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, Nat.cast_le]
exact (finrank_top K L).ge
exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α)
