Search for blocks/addresses/...
Proofgold Object
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
omega
)
(
∀ x4 : ο .
(
∀ x5 .
and
(
and
(
and
(
ap
x5
0
=
x0
)
(
ap
x5
x3
=
x1
)
)
(
∀ x6 .
x6
∈
ordsucc
x3
⟶
Field
(
ap
x5
x6
)
)
)
(
∀ x6 .
x6
∈
x3
⟶
∀ x7 : ο .
(
∀ x8 .
and
(
x8
∈
field0
(
ap
x5
(
ordsucc
x6
)
)
)
(
∀ x9 : ο .
(
∀ x10 .
and
(
x10
∈
omega
)
(
and
(
CRing_with_id_omega_exp
(
ap
x5
(
ordsucc
x6
)
)
x8
x10
∈
field0
(
ap
x5
x6
)
)
(
Field_extension_by_1
(
ap
x5
x6
)
(
ap
x5
(
ordsucc
x6
)
)
x8
)
)
⟶
x9
)
⟶
x9
)
⟶
x7
)
⟶
x7
)
⟶
x4
)
⟶
x4
)
⟶
x2
)
⟶
x2
type
ι
→
ι
→
ο
theory
HotG
name
radical_field_extension
definition
PUXQg..
Megalodon
radical_field_extension
proofgold address
TMZ6X..
radical_field_extension
creator
5919
Pr6Pc..
/
45a30..
owner
5919
Pr6Pc..
/
45a30..
term root
4b1aa..