instIsDomainSubtypeMem

Mathlib.Algebra.Ring.Subring.Defs

URI: https://scilib.ai/kg/mathlib#Subring.instIsDomainSubtypeMem

English

If R is a domain, then the subring s regarded as a Ring is a domain.

Русский

Если R — домен, то подкольцо s, как множество, образует домен.

LaTeX

$$$$ \text{IsDomain}(\text{Subtype } x\, (x\in s)) $$$$

Lean4

/-- A subring of a domain is a domain. -/
instance {R} [Ring R] [IsDomain R] (s : Subring R) : IsDomain s :=
  NoZeroDivisors.to_isDomain _

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

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

Разделы

Аффилиация

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