Proofgold Proposition

∀ x0 . x0 ∈ complex ⟶ (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ complex) (mul_CSNo x0 x2 = 1) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
nonzero_complex_recip_ex

proof
PUNr2..

Megalodon
nonzero_complex_recip_ex

proofgold address
TMVsi..^{nonzero_complex_recip_ex}

creator
12547 PrGxv../28143..

owner
12547 PrGxv../28143..

term root
4d750..