Email Gateway (Aug 22 2022 at 18:47): Email Gateway (Aug 22 2022 at 18:47):From: Anthony Bordg <bordg.anthony@gmail.com>
Dear all,
I noticed something weird with the definition of abelian monoids in
the Ring theory of the HOL-Algebra library.
Indeed, there one can find the following locale:
locale abelian_monoid =
fixes G (structure)
assumes a_comm_monoid:
"comm_monoid (add_monoid G)"
, and if one hovers over the G variable (with the cmd key) then one
notices that it is of type "('a, 'b) ring-scheme".
As a consequence, one needs a ring-scheme to define an abelian monoid!
Is there any good reason for that choice ?
Let assume that I need to prove that the set of 4-dimensional real
vectors, equipped with the obvious addition and zero, is an abelian
monoid,
do you suggest me to use the following record:
definition real4_monoid :: "(_, _) ring_scheme" where
"real4_monoid ≡ ⦇carrier = UNIV::(real^4) set, mult = real4_add, one =
real4_zero,
zero = undefined, add = undefined⦈" ?
Of course, the necessary (due to the fact noticed above) hack of using
"undefined" is not elegant, so one may want to fix the Algebra
library.
Best regards
Anthony
Last updated: Apr 18 2024 at 04:17 UTC