I see no ambiguity there; it's actually clear to me which gets used where. The use of infimum made perfect sense given that the supremum is what puts the 'g' in gcd; it's probably best that it be kept in that unseparately-defined limbo state lest needed support theorems blow up set.mm's size...
I'll admit I'm just happy to see lcm in the main area, and better elaborated! It was part of my own private experiments long ago now with Goldbach—or rather examinations of some proofs of it that are, well, "not generally accepted by the mathematical community" <https://primes.utm.edu/notes/crackpot.html>—that couldn't prove or disprove anything one way or another and really just went nowhere. My already-scant time for that or the Riemann-related stuff I'd hoped to try has since flatlined. On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens wrote: > > In my latest PR, I provided a function mapping a set of integers to their > least common multiple (~df-lcmf: ( _lcm `` s ) ) in addition to the > operation calculating the least common multiple of two integers (~df-lcm: ( > m lcm n ) ), contributed by SR. > > For the typesetting, however, I used the same representation "lcm" for > both symbols ` lcm ` and ` _lcm ` - because it is clear by the context > which definition is used. If you look at the theorems in section *6.1.10 The > least common multiple*, then there should be no doubt that this > overloaded representation is not a problem. Only the definitions look a > little bit strange. Actually, the typesettings *are *different: lcm used > as operation has a leading and a trailing blank, lcm used as function has > not (according to our typography conventions). > > If anbody has objections against this overloading, and suggestions how the > current typesettings could be improved, I am open to change it. > > By the way, it seems a little confusing at the first glance that the least > common multiple > is defined by a supremum. Actually, it is an infimum, because the inverse > of > "less than" ` ``' < ` is used to turn supremum into infimum - currently we > don't have infimum defined separately. Since this is noted in set.mm on > several occations. it may be worth to think about providing a separate > definition for infimum... > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f7d54936-15b4-4034-b648-a79dddbd307an%40googlegroups.com.
