English
For a polynomial p that splits via i, the natDegree of p.map i equals the cardinality of its roots: natDegree(p.map i) = card((p.map i).roots).
Русский
Для многочлена p, распадающегося через i, натуральная степень p.map i равна кардиналу множества его корней: natDegree(p.map i) = card((p.map i).roots).
LaTeX
$$$\operatorname{natDegree}((p.map\ i)) = \operatorname{card}((p.map\ i).\text{roots})$$$
Lean4
theorem natDegree_eq_card_roots' {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
(p.map i).natDegree = Multiset.card (p.map i).roots :=
by
by_cases hp : p.map i = 0
· rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]
obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)
rw [← splits_id_iff_splits, ← he] at hsplit
rw [← he] at hp
have hq : q ≠ 0 := fun h => hp (by rw [h, mul_zero])
rw [← hd, add_eq_left]
by_contra h
have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [h]
have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ ?_ hsplit).2 h'
· rw [map_id] at this
exact this hr
· rw [map_id]
exact mul_ne_zero (monic_multisetProd_X_sub_C _).ne_zero hq
