On Mon, Jan 13, 2020 at 12:45 PM Benoit <[email protected]> wrote:
> Thanks for the interesting link. I do not understand Buzzard's comment: > "It's completely safe because every single *theorem* where division by > 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its > statement." > How can you enforce that in the future, someone will not write a theorem > not satisfying this ? Or is it again a "gentleman's agreement" ? > It's a tautology, because this is what is meant by "division by 0 isn't allowed". Some theorems, like x * x^-1 = 1, only hold for nonzero arguments, so naturally any theorem stating this will have a nonzero assumption. No gentleman's agreement is necessary, as this is ensured by the soundness of the proof system. Other theorems, like (-x)^-1 = -(x^-1), are satisfied also when x = 0, but in this case evidently division by 0 *is* allowed. No attempt is made to avoid the statement of such theorems in lean, and it's one less hypothesis to check. (Of course, chances are that you will need to know x is nonzero eventually after you string together 3 or 4 division theorems, but you don't have to provide the hypothesis each time if some have taken advantage of this "hack".) Mario -- 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/CAFXXJSvu92qfHe75GpKK%3DFTGX8Z%2B62S8Xy6%2BwLRW5o8yc0RhDg%40mail.gmail.com.
