Theorem: Int.mod_mul (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
h : a % c = 0
⊢ a * b % c = 0
Tactic:
rw [Nat.mul_mod, h, zero_mul, Nat.zero_mod]
State after:
no goals