Commit 2025-08-29 10:14 2b31d005

chore(LinearAlgebra/Span/Basic): some API for toSpanSingleton (#29086) Adds LinearMap.toSpanSingleton_add and LinearMap.toSpanSingleton_smul. LinearMap.span_singleton_eq_range is LinearMap.range_toSpanSingleton.symm, kept it (for the sake of the name) but moved it so we can use range_toSpanSingleton as its proof. Renamed ContinuousLinearMap.toSpanSingleton_smul' to _smul and deleted the old _smul because everything in _smul' can be inferred when R is commutative, so it seemed natural to me to do so. Similarly, renamed MeasureTheory.condExpIndSMul_smul' to _smul and deleted the old _smul because everything can be inferred.