Commit 2025-08-07 22:25 23b849ef

View on Github →

feat: generalize opNNNorm_le_of_unit_nnnorm to semilinear maps (#28014) This also generalizes to complex-linear maps.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean

modified theorem ContinuousLinearMap.opNorm_le_of_unit_norm

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

modified theorem ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm