zeroLocus_insert_zero

Mathlib.RingTheory.Spectrum.Prime.Basic

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

← MathLib Explorer

English

Adding 0 to a generating set does not change the zero locus:

Русский

Добавление 0 к порождающему множеству не меняет нулевой локус:

LaTeX

$$$\\mathrm{zeroLocus}(\\mathrm{insert}\\,0\\, s) = \\mathrm{zeroLocus}(s).$$$

Lean4

@[simp]
theorem zeroLocus_insert_zero (s : Set R) : zeroLocus (insert 0 s) = zeroLocus s := by
  rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]

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

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

Разделы

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

Аффилиация

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