Proofgold Object

λ x0 x1 x2 . ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ RealsStruct_divides x0 x3 x1 ⟶ RealsStruct_divides x0 x3 x2 ⟶ x3 = RealsStruct_one x0

type
ι → ι → ι → ο

theory
HotG

name
RealsStruct_coprime

definition
PUVyd..

Megalodon
RealsStruct_coprime

proofgold address
TMX9Z..^{RealsStruct_coprime}

creator
5857 Pr6Pc../1ddae..

owner
5857 Pr6Pc../1ddae..

term root
4857f..