ker_eq

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#IsPerfectClosure.ker_eq

← MathLib Explorer

English

If L is PerfectRing p and i is IsPerfectClosure i p, then the kernel of i equals the p-nilradical of K.

Русский

Если L является PerfectRing p и IsPerfectClosure i p, то ядро i совпадает с p-нилрадикалом K.

LaTeX

$$RingHom.ker(i) = pNilradical(K,p)$$

Lean4

theorem ker_eq [PerfectRing L p] [IsPerfectClosure i p] : RingHom.ker i = pNilradical K p :=
  IsPRadical.ker_le'.antisymm (i.pNilradical_le_ker_of_perfectRing p)

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

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

Разделы

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

Аффилиация

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