Theorem ContinuousLinearMap.op_norm_mulLeftRight_le

Modification history

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore: rename op_norm to opNorm (#10185)

Deleted ContinuousLinearMap.op_norm_mulLeftRight_le View on Github →

2024-01-11 16:24

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore(Analysis/NormedSpace/OperatorNorm): remove `local instance` in favor of `letI` (#9653) …

Modified ContinuousLinearMap.op_norm_mulLeftRight_le View on Github →

2023-05-17 20:21

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

feat: port Analysis.NormedSpace.OperatorNorm (#3903)

Added ContinuousLinearMap.op_norm_mulLeftRight_le View on Github →