R : Type u_1
S : Type ?u.17315
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a
R : Type u_1
S : Type ?u.17315
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
refine' ⟨_, pow n⟩
R : Type u_1
S : Type ?u.17315
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ Nat.pred n • a) → IsSMulRegular M a
R : Type u_1
S : Type ?u.17315
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ', ← smul_eq_mul]
no goals
R : Type u_1
S : Type ?u.17315
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ Nat.pred n • a) → IsSMulRegular M a
exact of_smul _