map_rootOfSplits' — Mathlib

English

If f splits via i and hfd is nonzero, then f.eval₂ i (rootOfSplits' i hf hfd) = 0.

Русский

Если f распадается через i и hfd ≠ 0, то f.eval₂ i (rootOfSplits' i hf hfd) = 0.

LaTeX

$$$f\map i \text{ is split and } hfd:\deg(f.map i)\neq 0 \Rightarrow f.\eval\_2\ i\ (rootOfSplits'\ i\ hf\ hfd) = 0$$$

Lean4

theorem map_rootOfSplits' {f : K[X]} (hf : f.Splits i) (hfd) : f.eval₂ i (rootOfSplits' i hf hfd) = 0 :=
  Classical.choose_spec <| exists_root_of_splits' i hf hfd

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