From 119611bbaa07cf576bb1d1e71762abfc18550ec6 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 12 Sep 2026 14:31:19 +0800 Subject: [PATCH 1/2] feat(Topology/ContinuousMap): add coeFnCLM --- Mathlib/Topology/ContinuousMap/Algebra.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean index ff3d01f255b2b5..3990fb93bfd337 100644 --- a/Mathlib/Topology/ContinuousMap/Algebra.lean +++ b/Mathlib/Topology/ContinuousMap/Algebra.lean @@ -609,6 +609,12 @@ def coeFnLinearMap : C(α, M) →ₗ[R] α → M := { (coeFnAddMonoidHom : C(α, M) →+ _) with map_smul' := coe_smul } +/-- Coercion to a function as a `ContinuousLinearMap`. -/ +@[simps! apply] +def coeFnCLM : C(α, M) →L[R] (α → M) where + __ := coeFnLinearMap R + cont := continuous_coeFun + variable (M) in /-- Composition on the right by a continuous map, as a `ContinuousLinearMap`. -/ @[simps] From 308df64f8642bd42747d9a50bb50bef777948ccf Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Wed, 16 Sep 2026 13:57:18 +0800 Subject: [PATCH 2/2] apply suggestion --- Mathlib/Topology/ContinuousMap/Algebra.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/ContinuousMap/Algebra.lean b/Mathlib/Topology/ContinuousMap/Algebra.lean index 3990fb93bfd337..cae04722a8a0c6 100644 --- a/Mathlib/Topology/ContinuousMap/Algebra.lean +++ b/Mathlib/Topology/ContinuousMap/Algebra.lean @@ -611,10 +611,13 @@ def coeFnLinearMap : C(α, M) →ₗ[R] α → M := /-- Coercion to a function as a `ContinuousLinearMap`. -/ @[simps! apply] -def coeFnCLM : C(α, M) →L[R] (α → M) where +def coeFnCLM : C(α, M) →L[R] α → M where __ := coeFnLinearMap R cont := continuous_coeFun +@[simp] +lemma toLinearMap_coeFnCLM : (coeFnCLM R (α := α) (M := M)).toLinearMap = coeFnLinearMap R := rfl + variable (M) in /-- Composition on the right by a continuous map, as a `ContinuousLinearMap`. -/ @[simps]