Commit 2026-06-04 10:17 fb4d9bf2

feat(Analysis): pre/postcomposition by an isometry preserves the operator norm (#39969) Also create a separate section for the new series of similar lemmas. Note that a few lemmas had to change from f.toLinearIsometry.toContinuousLinearMap to f.toContinuousLinearEquiv.toContinuousLinearMap because the latter is the inferred coercion from LinearIsometryEquiv to ContinuousLinearMap. This is in line with our decision to deprioritise coercions from isos to homs (compared to coercions within isos). From MeanFourier