English
For L with splits of minpoly for every x ∈ E, the number of F-algebra homomorphisms from E to L equals the F-dimension of E over F, i.e., Nat.card (E →ₐ[F] L) = finrank F E.
Русский
Если для каждого x ∈ E минполином minpoly F x распадается в L, то число F-однородных отображений E→ₐ[F] L равно размерности E над F.
LaTeX
$$$\operatorname{Nat.card}(E\to_{F} L) = \operatorname{finrank} F E$$$
Lean4
/-- **Primitive element theorem**: a finite separable field extension `E` of `F` has a
primitive element, i.e. there is an `α ∈ E` such that `F⟮α⟯ = (⊤ : Subalgebra F E)`. -/
@[stacks 030N "The moreover part"]
theorem exists_primitive_element : ∃ α : E, F⟮α⟯ = ⊤ :=
by
rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
· let P : IntermediateField F E → Prop := fun K => ∃ α : E, F⟮α⟯ = K
have base : P ⊥ := ⟨0, adjoin_zero⟩
have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) :=
by
intro K β hK
obtain ⟨α, hK⟩ := hK
rw [← hK, adjoin_simple_adjoin_simple]
haveI : Infinite F := isEmpty_fintype.mp F_inf
obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β
exact ⟨γ, hγ.symm⟩
exact induction_on_adjoin P base ih ⊤
· exact exists_primitive_element_of_finite_bot F E
