toCancelCommMonoidWithZero

Mathlib.Algebra.Ring.Regular

URI: https://scilib.ai/kg/mathlib#NoZeroDivisors.toCancelCommMonoidWithZero

Lean4

/-- A commutative ring with no zero divisors is a `CancelCommMonoidWithZero`.

Note this is not an instance as it forms a typeclass loop. -/
abbrev toCancelCommMonoidWithZero [CommRing α] [NoZeroDivisors α] : CancelCommMonoidWithZero α :=
  { NoZeroDivisors.toCancelMonoidWithZero, ‹CommRing α› with }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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