no goals
F : Type ?u.1031657
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(zsmulRec (Int.ofNat n) f) = Int.ofNat n • ↑f
rw [zsmulRec, Int.ofNat_eq_coe, coe_nsmulRec, coe_nat_zsmul]
no goals
F : Type ?u.1031657
α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
n : ℕ
⊢ ↑(zsmulRec (Int.negSucc n) f) = Int.negSucc n • ↑f
rw [zsmulRec, negSucc_zsmul, coe_neg, coe_nsmulRec]