natDegree_eq_card_roots — Mathlib

English

For p ∈ K[X], if p ≠ 0 and splits over i, then deg p equals the cardinal of the roots of p.map i.

Русский

Для p ∈ K[X], если p ≠ 0 и распадается над i, то deg p равно кардиналу корней p.map 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 natDegree_eq_card_roots {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    p.natDegree = Multiset.card (p.map i).roots :=
  (natDegree_map i).symm.trans <| natDegree_eq_card_roots' hsplit

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