card_rootSet_eq_natDegree_iff_of_splits

English

Let f ∈ F[X] be nonzero and split over K via the map F → K. Then the number of distinct roots of f in K equals the degree of f if and only if f is separable.

Русский

Пусть f ∈ F[X] не равен нулю и распадается над K через отображение F → K. Тогда число различных корней f в K равно deg f тогда и только тогда, когда f раздельно.

LaTeX

$$For f ∈ F[X], if f ≠ 0 and f.Splits (\\mathrm{algebraMap} F K), then Fintype.card (f.rootSet K) = f.natDegree ↔ f.Separable$$

Lean4

theorem card_rootSet_eq_natDegree_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0) (h : f.Splits (algebraMap F K)) :
    Fintype.card (f.rootSet K) = f.natDegree ↔ f.Separable := by
  classical
    simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, natDegree_eq_card_roots h,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]

Похожие утверждения