Theorems · Definition · commutative algebra

WittVector.truncate

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

truncate n is a ring homomorphism that truncates x to its first n entries to obtain a TruncatedWittVector, which has the same base p as x.

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

21 results in Mathlib

Foundations

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

Assumes

CommRingFact