Theorems DER, DT and DEC would be easier to prove if switched in order

[darijgr]

My suggestion: Theorems DER, DT and DEC are easiest to prove in the order DEC -> DT -> DER.

You can prove Theorem DEC by induction, very much like you currently prove Theorem DER: Compare the row expansion of det(A) about the 1-st row with the column expansion of det(A) about the j-th column. There is one common term in both, which you can cancel out. All the other terms can be further expanded (the ones in the row expansion can be column-expanded about the j-th column by induction, while the ones in the column expansion can be row-expanded about the 1-st row by the definition of the determinant). Once this is done, you've got a sum of precisely the same terms written down.

Once Theorem DEC is thus proven, Theorem DT can be derived from it by induction quite trivially (match the row expansion of det(A) with the column expansion of det(A^t)). No need to average several determinants as you do it now! (Thus, in particular, the proof works in any characteristic.)

Once this is done, Theorem DER follows from DEC + DT in the same way as you currently derive Theorem DEC from DER + DT.

[rbeezer]

Aah, that is an interesting approach. I spent a long time (like two years) trying to decide which of the various major theorems about determinants to prove first (given a row-1 expansion as the definition). Eventually decided on the "ugly" proof of DER and everything else followed without being too ugly. I'll spend more time with this when I next sit down to work through some updates. Thanks for taking the time to make all these suggestions.

…

On 06/20/2017 03:41 AM, Darij Grinberg wrote: My suggestion: Theorems DER, DT and DEC are easiest to prove in the order DEC -> DT -> DER. You can prove Theorem DEC by induction, very much like you currently prove Theorem DER: Compare the row expansion of det(A) about the 1-st row with the column expansion of det(A) about the j-th column. There is one common term in both, which you can cancel out. All the other terms can be further expanded (the ones in the row expansion can be column-expanded about the j-th column by induction, while the ones in the column expansion can be row-expanded about the 1-st row by the definition of the determinant). Once this is done, you've got a sum of precisely the same terms written down. Once Theorem DEC is thus proven, Theorem DT can be derived from it by induction quite trivially (match the row expansion of det(A) with the column expansion of det(A^t)). No need to average several determinants as you do it now! (Thus, in particular, the proof works in any characteristic.) Once this is done, Theorem DER follows from DEC + DT in the same way as you currently derive Theorem DEC from DER + DT. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#87>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABy2cqM38uJu9giSb4dVT6nSgFCHuB8Gks5sF6HIgaJpZM4N_ZjU>.

[darijgr]

Not a big deal -- I just spent an hour or so looking through the text a year ago (I decided against using it in my class mainly because of its coverage; but I like various aspects of it), recorded these issues somewhere (I wasn't aware of FCLA being on github back then), then spent another half an hour today posting them today once I realized I could easily report them here rather than clog your mailbox.

Notice that my approach doesn't really reduce the "ugliness" of the proof of DER; it just shifts it into the proof of DEC. It removes the need for the "1/n" argument in the proof of DT, though.