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 ≠ 0 ∈ R 使 ab = 0。 所以我們稱 a 是 non zero-divisor 指如果 ab = 0，那 b 一定等於 0。

NonZeroDivisor : {R : 𝓤 ̇ } {{_ : Ring R}} (a : R) → 𝓤 ̇
NonZeroDivisor {_}{R} a = (b : R) → (a ⊗ b ＝ 𝟘R → b ＝ 𝟘R)