Re: [mizar] How to search for a lemma?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>The plan is to write (or rather to collect) theorems using
>the field operation about complex numbers

In our Coq library that we wrote for FTA (it's called "CCORN"
now, I think, don't ask me what it means) the + on the
complex numbers is just an instance of the + on arbitrary
additive monoids (or "LoopStr"s, really, it's the one that in
the MML is defined as "RLVECT_1:def 3").  Do you consider it
a good idea to recast the whole theory of NAT until COMPLEX
to use that operator?  It makes everything more uniform, of
course:  when you talk about other groups, like polynomials
or elements of a vector space or whatever, you don't need to
start developing all the basic lemmas all over again.

>I hope the integrity of MML will be much higher.

Yes, I really like the idea of putting everything in the
complex numbers as much as possible.  It also fits the way
systems like Mathematica behave, there if you type a number,
it really is a complex number.  That becomes very clear when
you apply something like a square root or logarithm.

Freek