dedekind/conceptdedekind_1_1algebra_1_1SatisfiesVectorSpaceAxioms.html

template<typename V, typename F, typename AddV std::plus<V>, typename AddF std::plus<F>, typename MultF std::multiplies<F>, typename Act std::multiplies<>>

concept dedekind::algebra::SatisfiesVectorSpaceAxioms =

    HasVectorSpaceOperators<V, F, Act> && requires(F a, F b, V x, V y) {

      { AddV{}(x, y) } -> std::same_as<V>;

      { Act{}(a, AddV{}(x, y)) } -> std::same_as<V>;

      { AddV{}(Act{}(a, x), Act{}(a, y)) } -> std::same_as<V>;


      { AddF{}(a, b) } -> std::same_as<F>;

      { Act{}(AddF{}(a, b), x) } -> std::same_as<V>;

      { AddV{}(Act{}(a, x), Act{}(b, x)) } -> std::same_as<V>;


      { MultF{}(a, b) } -> std::same_as<F>;

      { Act{}(MultF{}(a, b), x) } -> std::same_as<V>;

      { Act{}(a, Act{}(b, x)) } -> std::same_as<V>;


      requires(

          !requires { dedekind::category::unit<F>(MultF{}); } ||

          requires {

            {

              Act{}(dedekind::category::unit<F>(MultF{}), x)

            } -> std::same_as<V>;

          });

    }

dedekind::algebra::HasVectorSpaceOperators
Pragmatic vector-space check used by first reified vector carriers.
Definition vectorspace.cppm:120

dedekind::algebra::SatisfiesVectorSpaceAxioms
Operational witness of the core vector-space axiom signatures.
Definition vectorspace.cppm:139

dedekind::category::unit
constexpr T unit(Op)
The unit of Op at the carrier T, read as unit<T>(Op{}).
Definition species.cppm:287