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
http://isabelle.in.tum.de/sledgehammer.html, it would have proved your
goal automatically (and trivially).
Florian Haftmann wrote:
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