pNilradical_le_nilradical — Mathlib

English

For any commutative semiring R and p, the p-nilradical is always contained in the nilradical: pNilradical R p ≤ nilradical R.

Русский

Для любого коммутативного полупринципа R и p выполняется: pNilradical R p ⊆ nilradical R.

LaTeX

$$$$ pNilradical(R,p) \\le nilradical(R). $$$$

Lean4

theorem pNilradical_le_nilradical {R : Type*} [CommSemiring R] {p : ℕ} : pNilradical R p ≤ nilradical R :=
  by
  by_cases hp : 1 < p
  · rw [pNilradical, if_pos hp]
  simp_rw [pNilradical, if_neg hp, bot_le]

Похожие утверждения