instIsDomainLex

Mathlib.Algebra.Order.Ring.Synonym

URI: https://scilib.ai/kg/mathlib#instIsDomainLex

English

If R is a domain, then the Lex construction of R is a domain.

Русский

Если R — доменное кольцо, то Lex(R) тоже доменное.

LaTeX

$$$\text{IsDomain}(\mathrm{Lex}(R))$$$

Lean4

instance [Ring R] [h : IsDomain R] : IsDomain (Lex R) :=
  h

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

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

Разделы

Аффилиация

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