Hi all, I'd like to move my theorem fsumkthpow (giving the value of the finite sum of powers) into the main body of Metamath, since it's a 100 theorem. However, that depends on the definition of Bernoulli polynomials, which I define using my well-founded recursion theorems. This is a fairly large body of theorems, so I'd like to get opinions before moving the three sections that this requires up.
If there's support for this, is there support for reworking transfinite recursion to be a special case of well-founded recursion? tfr1 through 3 can be easily expressed by setting recs ( F ) = wrecs ( _E , On , F ). I'd like to make this the official definition of recs, since it expresses that the important part of recursion is well-foundedness, not anything special about the ordinals themselves. Any thoughts? -Scott -- 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/6b4ca276-ce77-4b8a-835b-49a5a405a8f5o%40googlegroups.com.
