Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsField Concept Referenceexport

The axiomatic field witness — a commutative ring whose multiplicative structure is an abelian group (zero excluded, by convention on is_invertible_v). More...

Concept definition

template<typename T, typename Add, typename Mult>
A Commutative Group.
Definition total.cppm:638
A Ring whose multiplication is commutative.
Definition total.cppm:811
The axiomatic field witness — a commutative ring whose multiplicative structure is an abelian group (...
Definition total.cppm:857

Detailed Description

The axiomatic field witness — a commutative ring whose multiplicative structure is an abelian group (zero excluded, by convention on is_invertible_v).

A field is a commutative ring in which every non-zero element has a multiplicative inverse. Canonical examples: ℚ, ℝ, ℂ, and the Gaussian rationals ℚ(i).

The concept composes two existing pieces of the category tower:

  1. IsCommutativeRing<T, Add, Mult> — ring laws plus commutativity of multiplication.
  2. IsAbelianGroup<T, Mult> — the multiplicative structure is itself an abelian group.

The strict mathematical definition — "every \emph{non-zero} element is multiplicatively invertible" — cannot be stated in a C++ concept (concepts reason about types, not values). A carrier opts into the multiplicative-group witness by specialising is_invertible_v<T, Mult> / inverse_trait<T, Mult> to assert the field-level claim; zero is understood excluded. This is the same mechanism the library already uses for additive inverses (e.g. is_invertible_v<Modular<N>, std::plus> = true).

Note
The concept is deliberately \emph{axiomatic}: no operator requirements, consistent with the category:total layer's convention that structural concepts check species traits rather than operator syntax. The operator-bearing witness — which additionally requires operator/, .inverse(), and std::divides — is dedekind::algebra::IsField, which \emph{builds on} this concept by composing it with IsDivisionRing.

Downstream call sites that currently reach for dedekind::algebra::HasFieldOperators will retarget to IsField<T, Add, Mult> once carriers such as Rational<Z>, Complex<R>, and the relevant composites register the full ring- plus multiplicative-group-trait specialisations. That work is tracked under epic #374 and in particular #371 (axiom-hook auto-lifter).