mathlib
22464cf6 - feat(analysis/normed_space/basic): `norm_matrix_lt_iff` (#12151)

Commit
4 years ago
feat(analysis/normed_space/basic): `norm_matrix_lt_iff` (#12151) A strict variant of `norm_matrix_le_iff`, using `pi_norm_lt_iff`
Author
Parents
Loading