Theorems · Definition · field theory
pNilradical
(R : Type u_1) → [inst : CommSemiring R] → ℕ → Ideal R
Given a natural number p, the p-nilradical of a ring is defined to be the
nilradical if p > 1 (pNilradical_eq_nilradical), and defined to be the zero ideal if p ≤ 1
(pNilradical_eq_bot'). Equivalently, it is the ideal consisting of elements x such that
x ^ p ^ n = 0 for some n (mem_pNilradical).
- Defined in
- Mathlib.FieldTheory.IsPerfectClosure
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Idealstatement · cited by 4,748
- Bot.botproof · cited by 4,720
- nilradicalproof · cited by 41
Cited by20
Results whose statement or proof uses this declaration.
- mem_pNilradicalstatement · cited by 4
- IsPRadical.ker_lestatement · cited by 3
- pNilradical_eq_botstatement · cited by 2
- pNilradical_eq_nilradicalstatement · cited by 2
- IsPRadical.injective_comp_of_pNilradical_eq_botstatement and proof · cited by 2
- IsPRadical.ker_le'statement · cited by 2
- pow_expChar_pow_inj_of_pNilradical_eq_botstatement and proof · cited by 1
- PerfectRing.pNilradical_eq_botstatement · cited by 1
- pNilradical_eq_bot'statement · cited by 1
- pNilradical_eq_bot_of_frobenius_injstatement · cited by 1
- pNilradical_le_nilradicalstatement · cited by 1
- RingHom.pNilradical_le_ker_of_perfectRingstatement and proof · cited by 1