Theorems · Theorem · field theory

Polynomial.roots_X_pow_char_sub_C_pow

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R} {m : ℕ}, ((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Defined in

Mathlib.FieldTheory.Perfect

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainExpCharPerfectRing