On October 4, 2019 9:32:33 PM EDT, Norman Megill <[email protected]> wrote: > >I defined pi earlier, but I don't think there were any theorems using >that >definition, so it doesn't really count. Use Paul's version. > >Norm
Instead of pi, let's use cos. That one has a much simpler history. Definition df-cos defines the cosine function. (Contributed by NM, 14-Mar-2005.) --- David A.Wheeler -- 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/AFD69340-4AA7-4034-8314-8955AE6D3D37%40dwheeler.com.
