Product_Distributes_over_Modulo_Operation
Disprovedmodular-arithmeticproofwiki
For integers x, y, z with y and z nonzero, z * (x mod y) = (z * x) mod (z * y).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Product_Distributes_over_Modulo_Operation (x y z : ℤ) (hy : y ≠ 0) (hz : z ≠ 0) : z * (x % y) = (z * x) % (z * y) := by sorry
Source