rootOfSplits — Mathlib

English

If p ≠ 0 and splits over i, then deg p equals the cardinality of the roots of p mapped by i.

Русский

Если p ≠ 0 и распадается над i, то deg p равно мощности множества корней p, отображённых через i.

LaTeX

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

Lean4

/-- Pick a root of a polynomial that splits. This version is for polynomials over a field and has
simpler assumptions. -/
def rootOfSplits {f : K[X]} (hf : f.Splits i) (hfd : f.degree ≠ 0) : L :=
  rootOfSplits' i hf ((f.degree_map i).symm ▸ hfd)

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