toCancelMonoidWithZero — Mathlib

English

An integral domain (a ring with no zero divisors) yields a CancelMonoidWithZero.

Русский

Целостный домен (кольцо без нулевых делителей) образует CancelMonoidWithZero.

LaTeX

$$CancelMonoidWithZero α$$

Lean4

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

Note this is not an instance as it forms a typeclass loop. -/
abbrev toCancelMonoidWithZero [Ring α] [NoZeroDivisors α] : CancelMonoidWithZero α
    where
  mul_left_cancel_of_ne_zero ha := (isRegular_of_ne_zero' ha).1
  mul_right_cancel_of_ne_zero hb := (isRegular_of_ne_zero' hb).2

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