R : Type u_1
S : Type ?u.9429
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
R : Type u_1
S : Type ?u.9429
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (?m.11206 h * b)
rw [h]
no goals
R : Type u_1
S : Type ?u.9429
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
exact one M