diff --git a/src/topology/continuous_function/bounded.lean b/src/topology/continuous_function/bounded.lean index 5168d1e1448b2..f3c1040617bd2 100644 --- a/src/topology/continuous_function/bounded.lean +++ b/src/topology/continuous_function/bounded.lean @@ -834,6 +834,9 @@ instance : has_scalar 𝕜 (α →ᵇ β) := @[simp] lemma coe_smul (c : 𝕜) (f : α →ᵇ β) : ⇑(c • f) = λ x, c • (f x) := rfl lemma smul_apply (c : 𝕜) (f : α →ᵇ β) (x : α) : (c • f) x = c • f x := rfl +instance [has_scalar 𝕜ᵐᵒᵖ β] [is_central_scalar 𝕜 β] : is_central_scalar 𝕜 (α →ᵇ β) := +{ op_smul_eq_smul := λ _ _, ext $ λ _, op_smul_eq_smul _ _ } + instance : has_bounded_smul 𝕜 (α →ᵇ β) := { dist_smul_pair' := λ c f₁ f₂, begin rw dist_le (mul_nonneg dist_nonneg dist_nonneg),