Theorem: Ring.inverse_pow_mul_eq_iff_eq_mul (DividedPowers/ForMathlib/AlgebraLemmas.lean)

State before:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ inverse a ^ k * b = c ↔ b = a ^ k * c
Tactic:
rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]
State after:
no goals