Theorems · Definition · commutative algebra
Perfection.coeff
(R : Type u_1) → [inst : CommSemiring R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [inst_1 : CharP R p] → ℕ → Perfection R p →+* R
The n-th coefficient of an element of the perfection.
- Defined in
- Mathlib.RingTheory.Perfection
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringFactCharP
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- MonoidHomproof · cited by 3,629
- Factstatement and proof · cited by 2,726
- Nat.Primestatement and proof · cited by 2,059
- CharPstatement and proof · cited by 478
- Perfectionstatement and proof · cited by 84
- Perfection.coeffMonoidHomproof · cited by 24
Cited by54
Results whose statement or proof uses this declaration.
- PreTilt.coeffproof · cited by 21
- Perfection.liftproof · cited by 8
- Perfection.extstatement and proof · cited by 7
- Perfection.mk_teichmullerstatement and proof · cited by 5
- Perfection.teichmullerAuxproof · cited by 4
- Perfection.coeff_add_ne_zerostatement and proof · cited by 3
- Perfection.teichmullerFun_sModEqstatement and proof · cited by 3
- Perfection.teichmullerFun_spec'statement and proof · cited by 3
- PreTilt.coeff_iterate_frobeniusEquiv_symmproof · cited by 3
- Perfection.coeff_ne_zero_of_lestatement and proof · cited by 2
- Perfection.coeff_pow_pstatement · cited by 2
- Perfection.teichmullerFun_specstatement and proof · cited by 2