Commit 2023-09-25 05:21 6f7f5f38
View on Github →feat(OperatorNorm,Multilinear): add lemmas, golf (#7302)
Analysis/NormedSpace/OperatorNorm
- Add
ContinuousLinearMap.isLeast_op_norm
,ContinuousLinearMap.op_nnnorm_le_iff
, andContinuousLinearMap.isLeast_op_nnnorm
. - Golf some proofs.
- Drop
RingHomIsometric
assumption here and there.
Analysis/NormedSpace/Multilinear
- Add
ContinuousMultilinearMap.isLeast_op_norm
,ContinuousMultilinearMap.isLeast_op_nnnorm
,ContinuousMultilinearMap.le_mul_prod_of_le_op_norm_of_le
,ContinuousMultilinearMap.op_norm_le_iff
,ContinuousMultilinearMap.op_nnnorm_le_iff
,ContinuousMultilinearMap.op_nnnorm_prod
,ContinuousMultilinearMap.op_nnnorm_pi
. - Golf/move some proofs.
- Change implicit/explicit arguments in some lemmas.