Benoît proposed to give a bird's eye view of the proof here (a good idea in principle), but I provided already a detailed documentation of the proof in set.mm itself (see comments of subsection "The Cayley-Hamilton theorem"), and I plan to improve/enhance it further in the next days. Hopefully, this documentation will be sufficient. So if you are interested in details, please look at http://us.metamath.org/mpeuni/mmtheorems313.html (caution: this link may not reference the page containing subsection "The Cayley-Hamilton theorem" in the future).
Alexander -- 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/58d22eb5-8dbf-4329-97aa-d8bee8ee4000%40googlegroups.com.
