instIsDomain

Mathlib.Algebra.Ring.Opposite

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

English

If R is a domain, then AddOpposite R is a domain.

Русский

Если R — доменная область, то AddOpposite R — доменная область.

LaTeX

$$$\text{IsDomain}(R) \Rightarrow \text{IsDomain}(\mathrm{AddOpposite}(R))$$$

Lean4

instance instIsDomain [Ring R] [IsDomain R] : IsDomain Rᵃᵒᵖ :=
  NoZeroDivisors.to_isDomain _

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

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

Разделы

Аффилиация

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