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
zmod_zmult_distrib:

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

Hope this helps
	Florian

P.S. tested with Isabelle 2008

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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