Re: [isabelle] mod_mult_distrib

Note that Proof General allows you to search for theorems using the Find button. If you type `intro', it will find all the theorems whose conclusion matches your current goal. If you install sledgehammer, it would have proved your goal automatically (and trivially).


Florian Haftmann wrote:
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

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