no goals
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
refine' ⟨fun h => _, fun h => _⟩ <;>
  simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
    star_star, star_one] using IsUnit.star h