pNilradical_one

Mathlib.FieldTheory.IsPerfectClosure

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

English

For any commutative semiring R, pNilradical R 1 = ⊥.

Русский

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

LaTeX

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

Lean4

theorem pNilradical_one {R : Type*} [CommSemiring R] : pNilradical R 1 = ⊥ :=
  pNilradical_eq_bot' rfl.le

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

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

Разделы

Аффилиация

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