Commit 2026-05-21 21:58 14a80078

View on Github →

refactor(Analysis): add toSpanSingleton isometry API (#38272)

rename ring_lmap_equiv_self to toSpanSingletonLIE and add basic supporting simp lemmas
moves this API under the existing toSpanSingleton naming scheme, and deprecates ring_lmap_equiv_selfₗ / ring_lmap_equiv_self, since these are just the corresponding toSpanSingleton maps under the old naming or as the symmetry of an existing definition

Estimated changes

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/Normed/Operator/Mul.lean

deleted def ContinuousLinearMap.ring_lmap_equiv_self

deleted def ContinuousLinearMap.ring_lmap_equiv_selfₗ

added theorem ContinuousLinearMap.toContinuousLinearEquiv_toSpanSingletonLIE

added theorem ContinuousLinearMap.toLinearEquiv_toSpanSingletonLIE

added def ContinuousLinearMap.toSpanSingletonLIE

added theorem ContinuousLinearMap.toSpanSingletonLIE_apply

added theorem ContinuousLinearMap.toSpanSingletonLIE_symm_apply

Modified Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean