Theorems · Theorem · commutative algebra
WittVector.eq_zero_of_p_mul_eq_zero
∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
(x : WittVector p k), x * ↑p = 0 → x = 0If k is a perfect ring of characteristic p, then the ring of Witt vectors 𝕎 k is
p-torsion free.
- Defined in
- Mathlib.RingTheory.WittVector.Complete
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FactCommRingCharPPerfectRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Factstatement and proof · cited by 2,726
- Nat.Primestatement and proof · cited by 2,059
- CharPstatement and proof · cited by 478
- WittVectorstatement and proof · cited by 227
- PerfectRingstatement and proof · cited by 154
- Function.Bijective.injectiveproof · cited by 115
- map_eq_zero_iffproof · cited by 62
- WittVector.verschiebungproof · cited by 32
- WittVector.frobeniusproof · cited by 22
- WittVector.frobenius_verschiebungproof · cited by 7
- WittVector.frobenius_bijectiveproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.