OP-00102 Lean verified Nobori's spectral-middle-factor commutator conjecture FA · Böttcher–Wenzel inequality · commutators · norm inequalities · OpenProblemsInNLA
OP-00108 Lean verified Constant one in the logarithmic commutator inequality FA · commutators · matrix logarithms · OpenProblemsInNLA
OP-00142 Open The complex Lu–Wenzel spectral conjecture FA · Böttcher–Wenzel inequality · commutators · eigenvalue inequalities · OpenProblemsInNLA