no goals
F : Type ?u.935054
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
⊢ ↑(nsmulRec 0 f) = 0 • ↑f
rw [nsmulRec, zero_smul, coe_zero]
no goals
F : Type ?u.935054
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : AddMonoid β
inst✝ : LipschitzAdd β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(nsmulRec (n + 1) f) = (n + 1) • ↑f
rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec n]