Commit 2024-01-06 09:51 95f4d793

feat(Analysis/Matrix): linfty_op_nnnorm agrees with the operator norm (#9476) The witness used in the proof is inspired by https://math.stackexchange.com/a/1119933/1896. Trying to weaken the field assumption used in the proof is largely meaningless, since we can't even state the theorem without it.