toCancelMonoidWithZero

Mathlib.Algebra.Ring.Regular

URI: https://scilib.ai/kg/mathlib#IsDomain.toCancelMonoidWithZero

English

If α is a domain, then it carries a CancelMonoidWithZero structure.

Русский

Если α является доменом, то на нём определено структурс CancelMonoidWithZero.

LaTeX

$$CancelMonoidWithZero α$$

Lean4

instance (priority := 100) toCancelMonoidWithZero [Semiring α] [IsDomain α] : CancelMonoidWithZero α where

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

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

Разделы

Аффилиация

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