Theorems · Theorem · commutative algebra

WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [inst_1 : CharP R p] [inst_2 : PerfectRing R p]
  (x : WittVector p R) (n : ℕ),
  ↑p ^ (n + 1) ∣ x - ∑ i ≤ n, (WittVector.teichmuller p) (((frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i

p ^ (n + 1) divides x minus the summation of the first n + 1 terms of the Teichmuller series.

Defined in

Mathlib.RingTheory.WittVector.TeichmullerSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRing