[isabelle] Matrix-Vector operation



Hi,

This may be trivial but I have a difficulty proving the following lemma:

lemma
  fixes  A :: "real^3^3"
    and x::"real^3"
assumes "A>0"
  shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "

where A is a positive definite diagonal matrix. Is there a lemma predefined
related to this?

Cheers
Omar



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.