Theorems · Definition · field theory

Polynomial.rootsExpandPowEquivRoots

{R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      (p : ℕ) →
        [ExpChar R p] →
          (f : Polynomial R) →
            [inst_3 : DecidableEq R] →
              [PerfectRing R p] → (n : ℕ) → ↥((Polynomial.expand R (p ^ n)) f).roots.toFinset ≃ ↥f.roots.toFinset

If f is a polynomial over a perfect integral domain R of characteristic p, then there is a bijection from the set of roots of Polynomial.expand R (p ^ n) f to the set of roots of f. It's given by x ↦ x ^ (p ^ n), see rootsExpandPowEquivRoots_apply.

Defined in

Mathlib.FieldTheory.Perfect

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainExpCharDecidableEqPerfectRing