[isabelle-dev] Smallest contribution ever (trace_mul_sym generalization)

Johannes Hölzl hoelzl at in.tum.de
Wed Jun 26 10:58:47 CEST 2013

Hi Stephen,

Am Dienstag, den 25.06.2013, 17:37 -0500 schrieb Stephen Nuchia:
> 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 pushed your bundle to the Isabelle repository!

Are you working on a formalization using the linear algebra in

 - Johannes

More information about the isabelle-dev mailing list