no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : A
⊢ r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using
  @units_smul_resolvent _ _ _ _ _ r r a