-- Field 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.Field.Defs
import Ring.Defs

-- Inversion is total as a graph, but its laws are required away from zero.
-- So inv(0) is still a value, and nothing asserts 0⁻¹ * 0 = 1.
predicate MultiplicativeInverse (A mul zero one inv : Set) :=
  FunctionBetween(inv, A, A)
  ∧
  (∀ x ∈ A, x ≠ zero →
    (call2(mul, inv(x), x) = one
      ∧ call2(mul, x, inv(x)) = one))

predicate DivisionSemiring (A add zero mul one inv : Set) :=
  IsSemiring(A, add, zero, mul, one)
  ∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))

predicate Semifield (A add zero mul one inv : Set) :=
  CommSemiring(A, add, zero, mul, one)
  ∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))

predicate DivisionRing (A add zero neg mul one inv : Set) :=
  IsRing(A, add, zero, neg, mul, one)
  ∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))

predicate IsFieldWithInverse (A add zero neg mul one inv : Set) :=
  IsCommRing(A, add, zero, neg, mul, one)
  ∧ (Nontrivial(A, zero, one) ∧ MultiplicativeInverse(A, mul, zero, one, inv))