Definition. Non zero-divisor [ring-0004]

module ring-0004 where

open import MLTT.Spartan

open import ring-0000
open Ring {{...}}

一個 Ring $R$ 中的元素 $a$ 是 zero divisor 就表示存在 $b \ne 0 \in R$ 使 $a b = 0$。 所以我們稱 $a$ 是 non zero-divisor 指如果 $ab=0$，那 $b$ 一定等於 $0$。

NonZeroDivisor : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → 𝓤 ̇
NonZeroDivisor {_}{R} a = (b : R) → (a · b ＝ 0r → b ＝ 0r)