Theorems · Theorem · commutative algebra

WittVector.verschiebung_nonzero

∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] {x : WittVector p R},
  x ≠ 0 → ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑WittVector.verschiebung)^[n] x'

Defined in

Mathlib.RingTheory.WittVector.Domain

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactCommRing