Commit 2026-10-21 16:48 4e006b96

View on Github →

feat(Analysis/Matrix/Normed): prove ‖A i j‖ ≤ ‖A‖ for the operator norm (#44969) This PR proves the bound ‖A i j‖ ≤ ‖A‖ for the operator norm.

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/Matrix/Normed.lean

added theorem Matrix.nnnorm_apply_le_frobenius_nnnorm

added theorem Matrix.nnnorm_apply_le_linfty_opNNNorm

added theorem Matrix.nnnorm_apply_le_nnnorm

deleted theorem Matrix.nnnorm_entry_le_entrywise_sup_nnnorm

added theorem Matrix.norm_apply_le_frobenius_norm

added theorem Matrix.norm_apply_le_linfty_opNorm

added theorem Matrix.norm_apply_le_norm

deleted theorem Matrix.norm_entry_le_entrywise_sup_norm

Modified Mathlib/NumberTheory/NumberField/House.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean