Re: Lm9 of xcmplx_1

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