pNilradical_eq_bot'

Mathlib.FieldTheory.IsPerfectClosure

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

English

For p ≤ 1, pNilradical R p equals the bottom ideal ⊥.

Русский

При p ≤ 1 pNilradical R p равен минимальному идеалу ⊥.

LaTeX

$$$$ pNilradical(R,p) = \\bot \\quad\\text{если } p \\le 1. $$$$

Lean4

theorem pNilradical_eq_bot' {R : Type*} [CommSemiring R] {p : ℕ} (hp : p ≤ 1) : pNilradical R p = ⊥ :=
  pNilradical_eq_bot (not_lt.2 hp)

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

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

Разделы

Аффилиация

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