Theorems · Theorem · commutative algebra

WittVector.ghostComponentModPPow_map_mk

∀ {R : Type u} [inst : CommRing R] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] (n : ℕ) (x : WittVector p R),
  (WittVector.ghostComponentModPPow n) ((WittVector.map (Ideal.Quotient.mk (Ideal.span {↑p}))) x) =
    (Ideal.Quotient.mk (Ideal.span {↑p} ^ (n + 1))) ((WittVector.ghostComponent n) x)

Defined in

Mathlib.RingTheory.Perfectoid.FontaineTheta

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFact