Theorems · Definition · field theory

AlgebraicClosure.finEquivRoots

{k : Type u} →
  [inst : Field k] →
    {K : Type u_1} →
      [inst_1 : Field K] →
        [inst_2 : DecidableEq K] →
          {i : k →+* K} →
            {f : AlgebraicClosure.Monics k} →
              (Polynomial.map i ↑f).Splits → Fin (↑f).natDegree ≃ ↥(Polynomial.map i ↑f).roots.toEnumFinset

If a monic polynomial f : k[X] splits in K, then it has as many roots (counting multiplicity) as its degree.

Defined in

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Cited by

2 results in Mathlib

Foundations

Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldDecidableEq