degree_eq_card_roots — Mathlib

English

Same as degree_eq_card_roots: if p ≠ 0 and splits over i, then deg p equals the number of roots of p.map i.

Русский

То же самое, что и ранее: deg p равно количеству корней p.map i при p ≠ 0 и распаде над i.

LaTeX

$$$\\forall p:\\ K[X],\\; p \\neq 0 \\land \\text{Splits}(i,p) \\Rightarrow \\deg(p) = \\operatorname{card}((p.map i).\\text{roots}).$$$

Lean4

theorem degree_eq_card_roots {p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : Splits i p) :
    p.degree = Multiset.card (p.map i).roots := by rw [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots hsplit]

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