Proofgold Object

λ x0 x1 . unpack_b_i x0 (λ x2 . λ x3 : ι → ι → ι . pack_b (Sep x2 (quotient (normal_subgroup_equiv x0 x1))) (λ x4 x5 . canonical_elt (normal_subgroup_equiv x0 x1) (x3 x4 x5)))

type
ι → ι → ι

theory
HotG

name
quotient_Group

definition
PUMaE..

Megalodon
quotient_Group

proofgold address
TMJpr..^{quotient_Group}

creator
4924 Pr6Pc../884df..

owner
4924 Pr6Pc../884df..

term root
97190..