case zero
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ Nat.zero)

case succ
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ Nat.succ n)
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)
induction' n with n hn
case zero
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
case zero
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ Nat.zero)
rw [pow_zero]
no goals
case zero
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
simp only [one]
case succ
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)
case succ
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ Nat.succ n)
rw [pow_succ]
no goals
case succ
R : Type u_1
S : Type ?u.11283
M : Type u_2
a b : R
s : S
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)
exact (ra.smul_iff (a ^ n)).mpr hn