Theorems · Definition · commutative algebra

TruncatedWittVector.truncate

{p n : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      [inst_1 : Fact (Nat.Prime p)] → {m : ℕ} → n ≤ m → TruncatedWittVector p m R →+* TruncatedWittVector p n R

A ring homomorphism that truncates a truncated Witt vector of length m to a truncated Witt vector of length n, for n ≤ m.

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

20 results in Mathlib

Foundations

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

Assumes

CommRingFact