pNilradical_prime

Mathlib.FieldTheory.IsPerfectClosure

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

← MathLib Explorer

English

If p is prime, 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_prime {R : Type*} [CommSemiring R] {p : ℕ} (hp : p.Prime) : pNilradical R p = nilradical R :=
  pNilradical_eq_nilradical hp.one_lt

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

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

Разделы

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

Аффилиация

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