Proofgold Proposition

∀ x0 x1 . radical_field_extension x0 x1 ⟶ ∀ x2 : ο . (Field x0 ⟶ Field x1 ⟶ subfield x0 x1 ⟶ ∀ x3 . x3 ∈ omega ⟶ ∀ x4 . ap x4 0 = x0 ⟶ ap x4 x3 = x1 ⟶ (∀ x5 . x5 ∈ ordsucc x3 ⟶ Field (ap x4 x5)) ⟶ (∀ x5 . x5 ∈ ordsucc x3 ⟶ ∀ x6 . x6 ∈ ordsucc x5 ⟶ subfield (ap x4 x6) (ap x4 x5)) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 : ο . (∀ x7 . and (x7 ∈ field0 (ap x4 (ordsucc x5))) (∀ x8 : ο . (∀ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x4 (ordsucc x5)) x7 x9 ∈ field0 (ap x4 x5)) (Field_extension_by_1 (ap x4 x5) (ap x4 (ordsucc x5)) x7)) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
radical_field_extension_E

proof
PUXQg..

Megalodon
radical_field_extension_E

proofgold address
TMYAu..^{radical_field_extension_E}

creator
5919 Pr6Pc../e9488..

owner
5919 Pr6Pc../e9488..

term root
04aa4..