R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective ((fun x => x * a)^[n])
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)
rw [IsRightRegular, ← mul_right_iterate]
no goals
R : Type u_1
a b : R
inst✝ : Monoid R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective ((fun x => x * a)^[n])
exact rra.iterate n