Library ▹ Algebra ▹ Rings
Definition 2.8.1.  Let R be a set, ⊕ : R × R → R be an operation on R, 0 ∈ R, ⊖ : R → R be a function, ⊙ : R × R → R be an operation on R, 1 ∈ R. We define:
(R, ⊕, 0, ⊖, ⊙, 1) forms a ring  :⇔  (R, ⊕, 0, ⊖) forms an abelian group and (R, ⊙, 1) forms a monoid and ⊙ is distributive over ⊕ and 0 is an absorbing element for ⊙ and ∀ a, b ∈ R : a ⊙ ⊖(b) = ⊖(a) ⊙ b = ⊖(a ⊙ b)  ⇔  (R, ⊕, 0, ⊖) forms an abelian group and (R, ⊙, 1) forms a monoid and ⊙ is distributive over ⊕  ⇔  (R, ⊕, 0, ⊙, 1) forms a semiring and ∀ a ∈ R : a ⊕ ⊖(a) = ⊖(a) ⊕ a = 0
Equivalence.  No proof.
References.
  • https://en.wikipedia.org/wiki/Ring_(mathematics)
  • https://mathworld.wolfram.com/UnitRing.html
  • https://proofwiki.org/wiki/Definition:Ring_with_Unity
  • https://ncatlab.org/nlab/show/ring
  • https://coq.inria.fr/library/Coq.setoid_ring.Ring_theory.html#ring_theory
  • https://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring
[View Source]