no goals
F : Type ?u.1196548
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ↑(npowRec 0 f) = ↑f ^ 0
rw [npowRec, pow_zero, coe_one]
no goals
F : Type ?u.1196548
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ↑(npowRec (n + 1) f) = ↑f ^ (n + 1)
rw [npowRec, pow_succ, coe_mul, coe_npowRec f n]