module ring-0007 where open import MLTT.Spartan open import ring-0000 open Ring {{...}}
- u 是 left unit 的意思是存在 v 使 u ⋅ v = 1
- u 是 right unit 的意思是存在 v 使 v ⋅ u = 1
is-left-unit : {R : 𝓤 ̇ } {{_ : Ring R}} → R → 𝓤 ̇ is-left-unit {_} {R} u = Σ v ꞉ R , u · v ＝ 1r is-right-unit : {R : 𝓤 ̇ } {{_ : Ring R}} → R → 𝓤 ̇ is-right-unit {_} {R} u = Σ v ꞉ R , v · u ＝ 1r