Just joined the list, still very much a beginner but I think the attached change is valid and desirable. The theorem trace_mul_sym in HOL/Multivariate_Analysis/Determinants.thy is not stated in full generality; relaxing the restriction that the factor matrices be individually square is valid. In fact, the original proof script succeeds unmodified.
I hope I am following proper "external contributor" protocol here. I did not do the full battery of recommended pre-commitment tests because I haven't yet figured out how to switch my Cygwin environment to point at the local mercurial repository but I was able to build the relevant session in the HOL directory with the change replicated there. I'm thinking I should spin up a VM or work under Linux for preparing changesets and keep my real work on the official release on my primary workstation. -swn The documentation for this change now outweighs the change itself by three orders of magnitude :-)
trace_mult_sym.hgbundle
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
