English
As above, given X finite and F : E → Multiset L, the dependent function type ∀ x : X, { l ∈ L // l ∈ F x } is finite.
Русский
Как выше, при конечности X и F : E → Multiset L, зависимый тип ∀ x : X, { l ∈ L // l ∈ F x } конечен.
LaTeX
$$$Fintype (\forall x : X, { l : L // l \in F x })$$$
Lean4
/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
theorem minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) :
minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 :=
by
refine (minpoly.unique _ _ (monic_X_pow_sub_C _ hσ.orderOf_pos.ne.symm) ?_ ?_).symm
· simp [← AlgEquiv.pow_toLinearMap, pow_orderOf_eq_one]
· intro q hq hs
rw [degree_eq_natDegree hq.ne_zero, degree_X_pow_sub_C hσ.orderOf_pos, Nat.cast_le, ← not_lt]
intro H
rw [aeval_eq_sum_range' H, ← Fin.sum_univ_eq_sum_range] at hs
simp_rw [← AlgEquiv.pow_toLinearMap] at hs
apply hq.ne_zero
simpa using
Fintype.linearIndependent_iff.mp
(((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_algHom_injective).comp _
(Subtype.val_injective.comp ((finEquivPowers hσ).injective)))
(q.coeff ∘ (↑)) hs ⟨_, H⟩
