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 trybulec@math.uwb.edu.pl 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 <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/-- Jesse Alama http://centria.di.fct.unl.pt/~alama/