finite_irreducibleComponents_of_isNoetherian

English

A Noetherian scheme has a finite number of irreducible components.

Русский

Нётерова схема имеет конечное число ирредуцируемых компонент.

LaTeX

$$$\\text{If }X\\text{ is Noetherian, then }\\{\\text{irreducible components of }X\\}\\text{ is finite.}$$$

Lean4

/-- A Noetherian scheme has a finite number of irreducible components. -/
@[stacks 0BA8]
theorem finite_irreducibleComponents_of_isNoetherian [IsNoetherian X] : (irreducibleComponents X).Finite :=
  NoetherianSpace.finite_irreducibleComponents

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