Commit 2025-12-09 14:57 b16832b5

View on Github →

feat: toSpanSingleton as a continuous linear equivalence (#32318)

  • Define ContinuousLinearMap.toSpanSingletonCLE.
  • Use it to golf a proof about ContDiffOn and deriv.

Estimated changes