isIntegral_iff_irreducibleSpace_and_isReduced

English

A scheme X is integral iff its underlying space is irreducible and X is reduced.

Русский

Схема X интегральна тогда и только тогда, когда её основание неприводимо и X редуцирована.

LaTeX

$$$\text{IsIntegral}(X) \iff (\operatorname{IrreducibleSpace}(|X|) \wedge \text{IsReduced}(X))$$$

Lean4

theorem isIntegral_iff_irreducibleSpace_and_isReduced : IsIntegral X ↔ IrreducibleSpace X ∧ IsReduced X :=
  ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => isIntegral_of_irreducibleSpace_of_isReduced X⟩

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