Theorems · Definition · commutative algebra
WittVector.coeff
{p : ℕ} → {R : Type u_1} → WittVector p R → ℕ → Rx.coeff n is the nth coefficient of the Witt vector x.
This concept does not have a standard name in the literature.
- Defined in
- Mathlib.RingTheory.WittVector.Defs
- Cited by
- 138 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- WittVectorstatement and proof · cited by 227
Cited by156
Results whose statement or proof uses this declaration.
- WittVector.extstatement and proof · cited by 29
- WittVector.truncateFunproof · cited by 21
- WittVector.mapFunproof · cited by 13
- WittVector.zero_coeffstatement and proof · cited by 12
- WittVector.coeff_frobenius_charPstatement and proof · cited by 9
- WittVector.ext_iffstatement and proof · cited by 9
- WittVector.out_truncateFunproof · cited by 7
- WittVector.verschiebung_coeff_succstatement · cited by 7
- WittVector.shiftproof · cited by 6
- WittVector.verschiebungFunproof · cited by 6
- WittVector.RecursionMain.succNthDefiningPolyproof · cited by 5
- WittVector.RecursionMain.succNthValstatement and proof · cited by 5