Theorems · Definition · commutative algebra
PreTilt
(O : Type u₂) → [CommRing O] → ℕ → Type u₂
Perfection of O/(p) where O is the ring of integers of K.
- Defined in
- Mathlib.RingTheory.Perfection
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Perfectionproof · cited by 84
- ModPproof · cited by 23
Cited by38
Results whose statement or proof uses this declaration.
- PreTilt.coeffstatement · cited by 21
- PreTilt.untiltstatement · cited by 8
- PreTilt.valAuxstatement and proof · cited by 7
- WittVector.fontaineThetaModPPowstatement and proof · cited by 5
- WittVector.fontaineThetastatement · cited by 5
- PreTilt.valAux_eqstatement and proof · cited by 4
- PreTilt.coeff_iterate_frobeniusEquiv_symmstatement and proof · cited by 3
- PreTilt.valstatement · cited by 3
- WittVector.ghostComponentModPPow_teichmuller_coeffstatement and proof · cited by 2
- PreTilt.valAux.congr_simpstatement and proof · cited by 2
- PreTilt.coeff_pow_pstatement and proof · cited by 2
- PreTilt.valAux_zerostatement · cited by 2