instIsDomain

Mathlib.Algebra.Ring.Shrink

URI: https://scilib.ai/kg/mathlib#Shrink.instIsDomain

English

If α is a semiring and IsDomain α, then Shrink α is IsDomain.

Русский

Если α — полукольцо-домен, то Shrink α также является доменом.

LaTeX

$$$(\text{Semiring } \alpha) \land (\text{IsDomain } \alpha) \Rightarrow \text{IsDomain}(\text{Shrink } \alpha)$$$

Lean4

instance [Semiring α] [IsDomain α] : IsDomain (Shrink.{v} α) :=
  (Shrink.ringEquiv α).isDomain

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

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

Разделы

Аффилиация

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