instIsDomainSubtypeMem — Mathlib

English

Let R be an integral domain and s a subring of R. Then s is an integral domain.

Русский

Пусть R — интегральный домен и s — подкольцо R. Тогда s является интегральным доменом.

LaTeX

$$$ \\operatorname{IsDomain}(R) \\Rightarrow \\operatorname{IsDomain}(s) $$$

Lean4

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

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