-- Ring definitions
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.Defs
import Group.Defs

predicate CommSemiring (A add zero mul one : Set) := IsSemiring(A, add, zero, mul, one) ∧ Commutative(A, mul)
predicate IsCommRing (A add zero neg mul one : Set) := IsRing(A, add, zero, neg, mul, one) ∧ Commutative(A, mul)
predicate Nontrivial (A zero one : Set) := zero ∈ A ∧ (one ∈ A ∧ zero ≠ one)
predicate NoZeroDivisors (A mul zero : Set) := ∀ x ∈ A, ∀ y ∈ A, call2(mul, x, y) = zero → (x = zero ∨ y = zero)
predicate IsIntegralDomain (A add zero neg mul one : Set) := IsCommRing(A, add, zero, neg, mul, one) ∧ (Nontrivial(A, zero, one) ∧ NoZeroDivisors(A, mul, zero))

notation scoped IsCommRing(R) => IsCommRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

notation scoped IsIntegralDomain(R) => IsIntegralDomain(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

notation scoped Nontrivial(R) => Nontrivial(R.carrier, R.zero, R.one)