A notable peculiarity of Algebra is its locale abelian_group, which is based on comm_group (groups with commutative multiplication) but with the weird twist of requiring a ring; it appears to be, in reality, the specification that a ring’s addition operator is commutative. Except that all rings have this property, and the very existence of this locale is confusing. Does anybody know any more about this?
record 'a ring = "'a monoid" +
zero :: 'a ("𝟬ı")
add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)
add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme"
where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one = zero R, … = (undefined :: 'm) ⦈"
locale abelian_monoid =
fixes G (structure)
"comm_monoid (add_monoid G)"
locale abelian_group = abelian_monoid +
"comm_group (add_monoid G)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and