degree_eq_card_roots' — Mathlib

English

For a nonzero p mapping that splits, degree equals the cardinality of its roots: degree(p.map i) = card((p.map i).roots).

Русский

Для непустого p, распадающегося через i, deg(p.map i) = card((p.map i).roots).

LaTeX

$$$\deg(p.map\ i) = \operatorname{card}((p.map\ i).\text{roots})$$$

Lean4

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

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