pNilradical_eq_bot

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#pNilradical_eq_bot

English

For any commutative semiring R, the p-nilradical at p = 1 is the bottom (zero) ideal: pNilradical R 1 = ⊥.

Русский

Для любого коммутативного полус семиринга R pNilradical R 1 = ⊥.

LaTeX

$$$$ pNilradical(R,1) = \\bot. $$$$

Lean4

theorem pNilradical_eq_bot {R : Type*} [CommSemiring R] {p : ℕ} (hp : ¬1 < p) : pNilradical R p = ⊥ := by
  rw [pNilradical, if_neg hp]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru