of_isDomain

Mathlib.RingTheory.AdicCompletion.Noetherian

URI: https://scilib.ai/kg/mathlib#IsHausdorff.of_isDomain

English

If R is a domain and I ≠ ⊤, then IsHausdorff I R holds (via isNoetherian framework).

Русский

Если R домен и I ≠ ⊤, тогда IsHausdorff I R выполняется.

LaTeX

$$$ IsHausdorff I R $$$

Lean4

theorem of_isDomain [IsDomain R] (h : I ≠ ⊤) : IsHausdorff I R :=
  .of_noZeroSMulDivisors I R h

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

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

Разделы

Аффилиация

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