Theorem ContinuousLinearMap.nnnorm_id

Modification history

2024-02-27 00:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore(Analysis/NormedSpace): split up OperatorNorm.lean (#10990) …

Modified ContinuousLinearMap.nnnorm_id View on Github →

2023-11-29 00:23

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

refactor(*/Multilinear): change `*.ofSubsingleton` (#8694) …

Added ContinuousLinearMap.nnnorm_id View on Github →