Proofgold Proposition

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

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