case intro
R : Type u_1
S : Type ?u.36377
M : Type u_2
b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a
R : Type u_1
S : Type ?u.36377
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a
rcases ua with ⟨a, rfl⟩
no goals
case intro
R : Type u_1
S : Type ?u.36377
M : Type u_2
b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a
exact a.isSMulRegular M