Theorems · Theorem · commutative algebra
WittVector.zero_coeff
∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ), WittVector.coeff 0 n = 0
- Defined in
- Mathlib.RingTheory.WittVector.Defs
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Factstatement and proof · cited by 2,726
- Nat.Primestatement and proof · cited by 2,059
- map_zeroproof · cited by 1,614
- Matrix.vecEmptyproof · cited by 832
- MvPolynomial.aevalproof · cited by 298
- WittVectorstatement · cited by 227
- WittVector.coeffstatement and proof · cited by 138
- WittVector.wittZeroproof · cited by 3
- WittVector.wittZero_eq_zeroproof · cited by 1
Cited by12
Results whose statement or proof uses this declaration.
- WittVector.verschiebung_nonzeroproof · cited by 2
- WittVector.p_nonzeroproof · cited by 2
- TruncatedWittVector.coeff_zeroproof · cited by 2
- WittVector.verschiebung_injectiveproof · cited by 1
- TruncatedWittVector.iInf_ker_truncateproof · cited by 1
- WittVector.mulN_coeffproof · cited by 1
- WittVector.frobeniusRotation_nonzeroproof · cited by 1
- WittVector.sum_coeff_eq_coeff_sumproof · cited by 1
- WittVector.mapFun.zeroproof · cited by 1
- WittVector.exists_frobenius_solution_fractionRing_auxproof · cited by 1
- WittVector.teichmuller_zeroproof · cited by 0
- WittVector.map_eq_zero_iffproof · cited by 0