intro hmod
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
⊢ b % c = 0 → a * b / c = a * (b / c)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)