Hi Benoît, the metamath theorem corresponding to equation (2) (called "fundamental relation of the adjugate" in Wikipedia) is ~ cpmadurid (see step 7. of the outline of the proof), which itself is a special case (for the characteristic matrix of a matrix) of ~ madurid , contributed by Stefan O'Rear in July 2018. So this theorem was already proven before Cramer's rule was available (which I proved in Februrary this year). I used ~ madurid indirectly for the proof of Cramer's rule (via ~ matinv , ~ matunit , ~ slesolinv , ~ slesolinvbi , ~ slesolex and ~ cramerlem3 ). This is the reason why Cramer's rule is not required to prove the Cayley Hamilton theorem.
Regards, Alexander On Thursday, December 12, 2019 at 1:00:35 PM UTC+1, Benoit wrote: > > Alexander, > I'm looking at the section comment of "21.25.10.3 The Cayley-Hamilton > theorem". What is the metamath label corresponding to Equation (2) ? I > see that ~cramer has no theorem referencing it. I thought the natural > proof of (2) would use Cramer's rule ? > Thanks, > Benoît > -- 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/5b9238d8-2870-4c60-aeaa-46182edd1235%40googlegroups.com.
