Proofgold Object

λ x0 . prim0 (λ x1 . and (x1 ∈ omega) (ccad8.. x1 {x2 ∈ ordsucc x0|and (0 ∈ x2) (coprime_nat x2 x0)}))

type
ι → ι

theory
HotG

name
-

definition
PUfRN..

Megalodon
-

proofgold address
TMTmT..

creator
4972 Pr6Pc../e0db4..

owner
4972 Pr6Pc../e0db4..

term root
64174..