1-- Field 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.Field.Defs8import Ring.Defs910-- Inversion is total as a graph, but its laws are required away from zero.11-- So inv(0) is still a value, and nothing asserts 0⁻¹ * 0 = 1.12predicate MultiplicativeInverse (A mul zero one inv : Set) :=13 FunctionBetween(inv, A, A)14∧15 (∀ x ∈ A, x ≠ zero →16 (call2(mul, inv(x), x) = one17∧ call2(mul, x, inv(x)) = one))1819predicate DivisionSemiring (A add zero mul one inv : Set) :=20 IsSemiring(A, add, zero, mul, one)21∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))2223predicate Semifield (A add zero mul one inv : Set) :=24 CommSemiring(A, add, zero, mul, one)25∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))2627predicate DivisionRing (A add zero neg mul one inv : Set) :=28 IsRing(A, add, zero, neg, mul, one)29∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))3031predicate IsFieldWithInverse (A add zero neg mul one inv : Set) :=32 IsCommRing(A, add, zero, neg, mul, one)33∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))34