[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] 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 <jesse.alama@gmail.com>:


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/