Proofgold Object

λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (explicit_Group x1 x2) (explicit_abelian x1 x2)))

type
ι → ο

theory
HotG

name
abelian_Group_alt

definition
PUdzs..

Megalodon
struct_b_abelian_group

proofgold address
TMKxi..^{struct_b_abelian_group}

creator
9727 PrCx1../63563..

owner
9727 PrCx1../63563..

term root
68631..