Commit 2025-03-11 08:53 b8035d11

View on Github →

chore(Topology/MetricSpace): rename BoundedSMul to IsBoundedSMul (#22797) ... and IsometricSMul / VAdd to IsIsometricSMul / VAdd.

Estimated changes

modified theorem IsUnit.integrable_smul_iff
modified theorem EMetric.infEdist_smul
modified theorem HolderWith.smul
modified theorem MemHolder.nnHolderNorm_smul
modified theorem MemHolder.nsmul
modified theorem MemHolder.smul
modified theorem eHolderNorm_nsmul
modified theorem eHolderNorm_smul
modified theorem Bornology.IsBounded.smul
modified theorem IsometryEquiv.divRight_symm
modified def IsometryEquiv.mulLeft
modified theorem IsometryEquiv.mulLeft_symm
modified theorem IsometryEquiv.mulRight_symm
modified theorem diam_smul
modified theorem dist_div_left
modified theorem dist_div_right
modified theorem dist_inv_inv
modified theorem dist_mul_left
modified theorem dist_mul_right
modified theorem dist_smul
modified theorem ediam_smul
modified theorem edist_div_left
modified theorem edist_div_right
modified theorem edist_inv
modified theorem edist_inv_inv
modified theorem edist_mul_left
modified theorem edist_mul_right
modified theorem edist_smul_left
modified theorem isometry_inv
modified theorem isometry_mul_left
modified theorem isometry_mul_right
modified theorem nndist_div_left
modified theorem nndist_div_right
modified theorem nndist_inv_inv
modified theorem nndist_mul_left
modified theorem nndist_mul_right
modified theorem nndist_smul