Proofgold Object

λ x0 x1 x2 . and (and (subfield x0 x1) (x2 ∈ setminus (field0 x1) (field0 x0))) (∀ x3 . subfield x0 x3 ⟶ x2 ∈ field0 x3 ⟶ subfield x1 x3)

type
ι → ι → ι → ο

theory
HotG

name
Field_extension_by_1

definition
PUXQg..

Megalodon
Field_extension_by_1

proofgold address
TMKZ3..^{Field_extension_by_1}

creator
5919 Pr6Pc../8dca8..

owner
5919 Pr6Pc../8dca8..

term root
15c0a..