theorem Matrix.norm_det_le_prod_norm_column {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] [LinearOrder n] [LocallyFiniteOrderBot n] [WellFoundedLT n] (A : Matrix n n 𝕜) : ‖A.det‖ ≤ ∏ j : n, √(∑ i : n, ‖A i j‖ ^ 2)

Hadamard's inequality (sharp form). The norm of the determinant of a square matrix over an RCLike field is at most the product of the Euclidean (L²) norms of its columns: ‖A.det‖ ≤ ∏ j, √(∑ i, ‖A i j‖ ^ 2).

This dominates the crude entrywise bound Matrix.det_le; equality holds precisely when the columns are pairwise orthogonal.