Hi Kunhao, Now that you have a mathbox, feel free to add to it this theorem (or maybe a more general version of it), it you feel like it!
set.mm also has the operation ` mod ` (see ~ df-mod), and I'm sure there is an easier and more natural way to describe that ` R ` relation using ` mod `, probably something around the lines of ` M R N <-> ( M mod 5 ) = ( N mod 5 ) ` for M, N in ZZ. BR, _ Thierry -- 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/1d5a7aba-f58e-9d81-1e75-5805665f4b8e%40gmx.net.
