Theorem Matrix.nnnorm_apply_le_linfty_opNNNorm

Modification history

2026-10-21 16:48
Mathlib/Analysis/Matrix/Normed.lean
feat(Analysis/Matrix/Normed): prove `‖A i j‖ ≤ ‖A‖` for the operator norm (#44969) …
Added Matrix.nnnorm_apply_le_linfty_opNNNormView on Github →