Email Gateway (Aug 18 2022 at 12:42): Email Gateway (Aug 18 2022 at 12:42):From: barzan stefania <stefania_barzan@yahoo.com>
Hi all!
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)
Thank you, Stefania Barzan
Email Gateway (Aug 18 2022 at 12:42):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 18 2022 at 12:42):From: Tobias Nipkow <nipkow@in.tum.de>
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).
Tobias
Florian Haftmann wrote:
Last updated: May 03 2024 at 12:27 UTC