Theorems · Theorem · commutative algebra

WittVector.mem_span_p_pow_iff_le_coeff_eq_zero

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
  (x : WittVector p k) (n : ℕ), x ∈ Ideal.span {↑p ^ n} ↔ ∀ m < n, x.coeff m = 0

If k is a perfect ring of characteristic p, a Witt vector x : 𝕎 k falls in ideal generated by p ^ n if and only if its initial n coefficients are 0.

Defined in

Mathlib.RingTheory.WittVector.Complete

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRing