pNilradical_eq_bot

Mathlib.FieldTheory.IsPerfectClosure

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

← MathLib Explorer

English

For a PerfectRing R with parameter p, the p-nilradical equals the bottom: pNilradical R p = ⊥.

Русский

Для идеального кольца R с параметром p выполняется pNilradical R p = ⊥.

LaTeX

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

Lean4

theorem pNilradical_eq_bot (R : Type*) [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] : pNilradical R p = ⊥ :=
  pNilradical_eq_bot_of_frobenius_inj R p (injective_frobenius R p)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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