[isabelle] abelian_group



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?

Larry

record 'a ring = "'a monoid" +
  zero :: 'a ("𝟬ı")
  add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65)

abbreviation
  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)
  assumes a_comm_monoid:
     "comm_monoid (add_monoid G)"

locale abelian_group = abelian_monoid +
  assumes a_comm_group:
     "comm_group (add_monoid G)"





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.