Theorem: ndiv_mul_right (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ a * b % p ≠ 0 → b % p ≠ 0
Tactic:
rw [Nat.mul_comm]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ b * a % p ≠ 0 → b % p ≠ 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ b * a % p ≠ 0 → b % p ≠ 0
Tactic:
exact ndiv_mul_left b a p
State after:
no goals