rootOfSplits' — Mathlib

English

rootOfSplits' i hf hfd is a chosen root of a polynomial f that splits with i, provided deg(f.map i) ≠ 0.

Русский

rootOfSplits' i hf hfd — это выбранный корень многочлена f, который распадается через i, при условии deg(f.map i) ≠ 0.

LaTeX

$$$\text{rootOfSplits}'\ i\ hf\ hfd \in L \quad\text{and}\quad eval_i(\text{rootOfSplits}'\ i\ hf\ hfd, f) = 0$$$

Lean4

/-- Pick a root of a polynomial that splits. See `rootOfSplits` for polynomials over a field
which has simpler assumptions. -/
def rootOfSplits' {f : K[X]} (hf : f.Splits i) (hfd : (f.map i).degree ≠ 0) : L :=
  Classical.choose <| exists_root_of_splits' i hf hfd

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