Theorem Matrix.norm_apply_le_frobenius_norm

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.norm_apply_le_frobenius_normView on Github →