Re: [isabelle] mod_mult_distrib

Dear Stefania,

> I want to prove mod_mult_distrib: "(a*b) mod (c::int)= ((a mod c) * (b mod c)) mod c". A similar property is already proved for a, b c natural numbers. I will like to have it for positive, nonzero integers. 
> Can someone give me an idea how to prove it? (maybe by using the property for nat)

Others have already done the work you :-)  The theorem is named

  "(a * b) mod (c::int)= ((a mod c) * (b mod c)) mod c"
  by (fact zmod_zmult_distrib)

Hope this helps

P.S. tested with Isabelle 2008



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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