R : Type u_2
S : Type u_1
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
R : Type u_2
S : Type u_1
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)
rw [h]
no goals
R : Type u_2
S : Type u_1
M : Type u_3
a b : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
exact one M