mathlib3

feat(analysis/von_neumann_algebra/basic): one result

#18290

Open