Theorems · Theorem · commutative algebra

WittVector.ghostComponent_teichmuller

∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (r : R) (n : ℕ),
  (WittVector.ghostComponent n) ((WittVector.teichmuller p) r) = r ^ p ^ n

The n-th ghost component of teichmuller p r is r ^ p ^ n.

Defined in

Mathlib.RingTheory.WittVector.Teichmuller

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactCommRing