no goals
ι : Type ?u.177283
α : Type ?u.177286
X : Type ?u.177289
M : Type u_1
N : Type ?u.177295
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous fun a => a ^ 0
simpa using continuous_const
ι : Type ?u.177283
α : Type ?u.177286
X : Type ?u.177289
M : Type u_1
N : Type ?u.177295
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k
ι : Type ?u.177283
α : Type ?u.177286
X : Type ?u.177289
M : Type u_1
N : Type ?u.177295
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a ^ (k + 1)
simp only [pow_succ]
no goals
ι : Type ?u.177283
α : Type ?u.177286
X : Type ?u.177289
M : Type u_1
N : Type ?u.177295
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k
exact continuous_id.mul (continuous_pow _)