Theorems · Theorem · field theory

Polynomial.roots_expand_pow

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
  [inst_3 : PerfectRing R p],
  ((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots

Defined in

Mathlib.FieldTheory.Perfect

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainExpCharPerfectRing