Theorems · Theorem · commutative algebra

WittVector.mem_span_p_iff_coeff_zero_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), x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0

If k is a perfect ring of characteristic p, a Witt vector x : 𝕎 k falls in ideal generated by p if and only if its zeroth coefficient is 0.

Defined in

Mathlib.RingTheory.WittVector.Complete

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRing