pNilradical_eq_nilradical

Mathlib.FieldTheory.IsPerfectClosure

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

← MathLib Explorer

English

If p is a prime number, then pNilradical R p equals nilradical R.

Русский

Если p — простое число, то pNilradical R p равно nilradical R.

LaTeX

$$$$ pNilradical(R,p) = nilradical(R) \\quad\\text{если } p\\text{ простое}. $$$$

Lean4

theorem pNilradical_eq_nilradical {R : Type*} [CommSemiring R] {p : ℕ} (hp : 1 < p) : pNilradical R p = nilradical R :=
  by rw [pNilradical, if_pos hp]

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

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

Разделы

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

Аффилиация

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