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/04c45c79-2f1f-4827-8623-1c9f1fa1e114n%40googlegroups.com.
