Theorem Matrix.nnnorm_apply_le_frobenius_nnnorm

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_frobenius_nnnormView on Github →