English
If f splits over i, then there is a canonical bijection between the finite degree of f and the roots of f in the splitting field.
Русский
Если f делится над i, существует естественная биекция между количеством корней f и корнями f в разбиении поля.
LaTeX
$$$\\mathrm{finEquivRoots}\\; hf : \\mathrm{Fin}(f.1.natDegree) \\simeq (f.1.map\\ i).\\mathrm{roots}.toEnumFinset$$$
Lean4
/-- If a monic polynomial `f : k[X]` splits in `K`,
then it has as many roots (counting multiplicity) as its degree. -/
def finEquivRoots {K} [Field K] [DecidableEq K] {i : k →+* K} {f : Monics k} (hf : f.1.Splits i) :
Fin f.1.natDegree ≃ (f.1.map i).roots.toEnumFinset :=
.symm <|
Finset.equivFinOfCardEq <| by
rwa [← splits_id_iff_splits, splits_iff_card_roots, ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf
