Proofgold Object

λ x0 x1 . ∃ x2 . and (x2 ∈ omega) (∃ x4 . and (and (and (ap x4 0 = x0) (ap x4 x2 = x1)) (∀ x6 . x6 ∈ ordsucc x2 ⟶ Field (ap x4 x6))) (∀ x6 . x6 ∈ x2 ⟶ ∃ x7 . and (x7 ∈ field0 (ap x4 (ordsucc x6))) (∃ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x4 (ordsucc x6)) x7 x9 ∈ field0 (ap x4 x6)) (Field_extension_by_1 (ap x4 x6) (ap x4 (ordsucc x6)) x7)))))

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..