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

[Johannes Hölzl]

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!
  http://isabelle.in.tum.de/repos/isabelle/rev/e64c1344f21b

Are you working on a formalization using the linear algebra in
Determinants?


 - Johannes