English
For a commutative semiring R and a natural number p, the p-nilradical is defined to be the nilradical when p > 1 and the zero ideal when p ≤ 1. Equivalently, it consists of elements x such that x^{p^n} = 0 for some n.
Русский
Для коммутативного полюса кольца R и натурального p, pNilradical определяется как nilradical, если p > 1, и как максимальная нулевая идеальная часть, если p ≤ 1. Эквивалентно, состоит из элементов x, для которых существует n: x^{p^n} = 0.
LaTeX
$$$$ pNilradical(R,p) = \\begin{cases} nilradical(R) & \\text{если } 1 < p, \\\\ ⊥ & \\text{если } p \\le 1. \\end{cases} $$$$
Lean4
/-- 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`). -/
def pNilradical (R : Type*) [CommSemiring R] (p : ℕ) : Ideal R :=
if 1 < p then nilradical R else ⊥
