Theorems · Definition · commutative algebra

WittVector.verschiebung

{p : ℕ} → {R : Type u_1} → [inst : CommRing R] → [hp : Fact (Nat.Prime p)] → WittVector p R →+ WittVector p R

verschiebung x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verschiebung x).coeff (i + 1). This is an additive monoid hom with underlying function verschiebung_fun.

Defined in

Mathlib.RingTheory.WittVector.Verschiebung

Cited by

32 results in Mathlib

Foundations

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

Assumes

CommRingFact