Grace/Cumulus/Algebra/Ring/Defs.g17

Open in Workbench Download source

Imports

Group.Defs

Declarations

• CommSemiring predicate
• IsCommRing predicate
• Nontrivial predicate
• NoZeroDivisors predicate
• IsIntegralDomain predicate

Source

1-- Ring definitions2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Ring.Defs8import Group.Defs910predicate CommSemiring (A add zero mul one : Set) := IsSemiring(A, add, zero, mul, one) ∧ Commutative(A, mul)11predicate IsCommRing (A add zero neg mul one : Set) := IsRing(A, add, zero, neg, mul, one) ∧ Commutative(A, mul)12predicate Nontrivial (A zero one : Set) := zero ∈ A ∧ (one ∈ A ∧ zero ≠ one)13predicate NoZeroDivisors (A mul zero : Set) := ∀ x ∈ A, ∀ y ∈ A, call2(mul, x, y) = zero → (x = zero ∨ y = zero)14predicate IsIntegralDomain (A add zero neg mul one : Set) := IsCommRing(A, add, zero, neg, mul, one) ∧ (Nontrivial(A, zero, one) ∧ NoZeroDivisors(A, mul, zero))1516notation scoped IsCommRing(R) => IsCommRing(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)1718notation scoped IsIntegralDomain(R) => IsIntegralDomain(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)1920notation scoped Nontrivial(R) => Nontrivial(R.carrier, R.zero, R.one)21