Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . CSNo x0∀ x1 . SNo x1mul_SNo (add_SNo (mul_SNo (CSNo_Re x0) (CSNo_Re x0)) (mul_SNo (CSNo_Im x0) (CSNo_Im x0))) x1 = 1mul_CSNo x0 (add_CSNo (mul_CSNo x1 (CSNo_Re x0)) (minus_CSNo (mul_CSNo Complex_i (mul_CSNo x1 (CSNo_Im x0))))) = 1
as obj
-
as prop
f9fad..CSNo_relative_recip
theory
HotG
stx
93147..
address
TMFKt..CSNo_relative_recip