Theorems · Definition · commutative algebra
TruncatedWittVector.coeff
{p n : ℕ} → {R : Type u_1} → Fin n → TruncatedWittVector p n R → Rx.coeff i is the ith entry of x.
- Defined in
- Mathlib.RingTheory.WittVector.Truncated
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 3 from the axioms · 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.
- TruncatedWittVectorstatement and proof · cited by 56
Cited by16
Results whose statement or proof uses this declaration.
- TruncatedWittVector.outproof · cited by 13
- TruncatedWittVector.extstatement and proof · cited by 7
- WittVector.coeff_truncatestatement · cited by 4
- WittVector.coeff_truncateFunstatement and proof · cited by 4
- TruncatedWittVector.coeff_mkstatement · cited by 2
- TruncatedWittVector.coeff_outstatement and proof · cited by 2
- TruncatedWittVector.coeff_zerostatement · cited by 2
- WittVector.truncate_liftFunproof · cited by 1
- WittVector.frobenius_frobeniusRotationproof · cited by 1
- TruncatedWittVector.coeff_truncatestatement and proof · cited by 1
- WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zeroproof · cited by 1
- TruncatedWittVector.ext_iffstatement and proof · cited by 1