R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ ↑(flip (mul R A)) a ^ n = ↑(flip (mul R A)) (a ^ n)
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulRight R a ^ n = mulRight R (a ^ n)
simp only [mulRight, ← Algebra.coe_lmul_eq_mul]
no goals
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ ↑(flip (mul R A)) a ^ n = ↑(flip (mul R A)) (a ^ n)
exact
  LinearMap.coe_injective (((mulRight R a).coe_pow n).symm ▸ mul_right_iterate a n)