Re: Re: Lm9 of xcmplx_1

Jesse,

Look here:

theorem :: XCMPLX_1:89
for b, a being complex number st b <> 0 holds
a = (a * b) / b by Lm9;

Best,

Adam

On Sun, 18 Mar 2012, Jesse Alama wrote:

>  http://www.mizar.org/version/current/html/xcmplx_1.html#E62
>
> you can see that the theorem I have in mind is called Lm9 and it is
> unexported.  I see this also in the .miz file for the official release
> of MML 4.181.1147.  Do you see this as well?  In xreal_1.abs I see
>
> :: [ xreal_1.abs ] ::::::::::::::::::::::::::::::::::::::::::::::::::::
>
> :: snip
>
> theorem :: XCMPLX_1:53 :: REAL_2'31
>  c <> 0 & a / c = b / c implies a = b;
>
> theorem :: XCMPLX_1:54 :: REAL_2'74
>  a / b <> 0 implies b = a / (a / b);
>
> :: snip
>
> ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
>
> with no such lemma (as expected, since it is not exported).
>
> Jesse
>
> [email protected] writes:
>
>> Is it Lm9? I have
>>
>> Lm9: b<>0 implies a=a*b/b
>>
>> and it seems that it is so for long time.
>>
>> Anyway, you need the theorem
>>
>> theorem :: XCMPLX_1:52  a <> 0 implies a / (a / b) = b;
>>
>> Maybe in version that you use it has a different number.
>>
>> Lemmas are often proved because the order in which we prove and the
>> order in which we
>> want to list theorems in abstract are different. Then they are
>> repeated as theorems with the justification "by lemma".
>>
>> I have checked lemmas in XCMPLX_1. All are exported as theorems:
>>
>> theorem :: REAL_1'24
>>  a" * b" = (a * b)" by Lm1;
>> theorem :: REAL_1'42
>>  a / (b / c) = (a * c) / b by Lm2;
>> theorem :: REAL_1'43
>>  b <> 0 implies a / b * b = a by Lm3;
>> theorem :: REAL_1'33_1
>>  1 / a = a" by Lm4;
>> theorem :: REAL_1'37
>>  a <> 0 implies a / a = 1 by Lm5;
>> theorem :: REAL_1'35
>>  (a / b) * (c / d) = (a * c) / (b * d) by Lm6;
>> theorem :: REAL_1'81
>>  (a / b)" = b / a by Lm7;
>> theorem :: SQUARE_1'18
>>  a * (b / c) = (a * b) / c by Lm8;
>> theorem :: REAL_2'62_2
>>  b <> 0 implies a = a * b / b by Lm9;
>> theorem :: REAL_1'38
>>  c <> 0 implies a / b = (a * c) / (b * c) by Lm10;
>> theorem :: REAL_2'47_1
>>   (a * b")" = a" * b by Lm11;
>> theorem :: REAL_2'33_1
>>  a" = b" implies a = b by Lm12;
>> theorem :: REAL_1'82
>>  (a / b) / (c / d) = (a * d) / (b * c) by Lm13;
>> theorem :: REAL_2'56:
>>  a * (1 / b) = a / b by Lm14;
>> theorem :: REAL_2'67_4
>>  1 / c * (a / b) = a / (b * c) by Lm15;
>> theorem :: REAL_1'33_2
>>  1 / a" = a by Lm16;
>> theorem :: REAL_1'39_1
>>  -a / b = (-a) / b by Lm17;
>> theorem :: REAL_2'46_1
>>  a <> 0 & a = a" implies a = 1 or a = -1 by Lm18;
>> theorem :: REAL_2'45_1
>>  (- a)" = -a" by Lm19;
>>
>> Greetings,
>> Andrzej
>>
>>
>> Cytowanie Jesse Alama <[email protected]>:
>>
>>> Please promote Lm9 of XCMPLX_1 (MML 4.181.1147)
>>>
>>> for a, b being complex number
>>>  st a <> 0 holds
>>>  a / (a / b) = b
>>>
>>> to a proper theorem.  It is quite silly to repeat the proof of this
>>> fact in an article.
>>>
>>> Imagine if a mathematician stated and proved this lemma in a paper on
>>> advanced complex analysis, with an apology: "The author of this useful
>>> lemma forbade me from citing it, so I have to reinvent this little
>>> wheel.  Let a and b be complex numbers, and assume that a is
>>> nonzero. ..."
>>>
>>> In fact, why not promote *all* the lemmas of XCMPLX_1 to proper
>>> theorems?  In this kind of article (part of the Encyclopedia), its many
>>> lemmas might be useful in many contexts.  No private lemmas, please!
>>>
>>> More generally, I am not convinced of the value of unexported
>>> theorems.  Neither an author nor the MML Library Committee knows just
>>> when a lemma might be useful for other people in contexts they don't
>>> currently work with.  Sure, in the course of writing an article (or
>>> maintaining it in light of other changes to the library), it might
>>> feel right to "hide" a lemma because it seems, at the time of writing,
>>> too specialized and therefore likely to have little reuse value to
>>> other authors.  And for the purposes of a JFM version of an article,
>>> maybe it is reasonable to suppress some excessively
>>> specialized/customized lemmas.  But with a growing MML, and greater
>>> reuse of more and more of its articles, I fail to see the value in
>>> hiding anything at all.  Expose all theorems and let the community of
>>> users of the MML, not the author of a particular article, decide which
>>> lemmas are important.
>>>
>>> Even if one disagrees with this general view of unexported theorems, I
>>> still think that for articles like XCMPLX_1, which are supposed to lay
>>> out a large variety of useful theorems, I fail to see the value in
>>> keeping any theorem private (unexported).
>>>
>>> Jesse
>>>
>>> --
>>> Jesse Alama
>>> http://centria.di.fct.unl.pt/~alama/
>>>
>>
>>
>>
>
> -- 
> Jesse Alama
> http://centria.di.fct.unl.pt/~alama/
>