isIrreducible_zeroLocus_iff

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.isIrreducible_zeroLocus_iff

← MathLib Explorer

English

IsIrreducible (zeroLocus I) iff radical(I) is prime.

Русский

IsIrreducible(zeroLocus(I)) эквивалентно радикал(I) прост.

LaTeX

$$$\\mathrm{IsIrreducible}(\\mathrm{zeroLocus}(I)) \\iff I^{\\mathrm{radical}}.\\mathrm{IsPrime}$$$

Lean4

theorem isIrreducible_zeroLocus_iff (I : Ideal R) : IsIrreducible (zeroLocus (I : Set R)) ↔ I.radical.IsPrime :=
  zeroLocus_radical I ▸ isIrreducible_zeroLocus_iff_of_radical _ I.radical_isRadical

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

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

Разделы

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

Аффилиация

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