instIsDomain

Mathlib.Algebra.Field.IsField

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

English

A semifield is a domain; i.e., it has no zero divisors and cancellation holds.

Русский

Семифилд является областью, то есть не имеет нулевых делителей и выполняются правила отмены.

LaTeX

$$$Semifield\,R \Rightarrow IsDomain\,R$$$

Lean4

instance {R : Type u} [Semifield R] : IsDomain R :=
  (Semifield.toIsField _).isDomain

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

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

Разделы

Аффилиация

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