Commit 2022-08-25 03:05 fec8ffec
View on Github →chore(analysis/normed_space/star/*): migrate use of a ∈ self_adjoint A to is_self_adjoint a (#16212)
After #15326, this PR migrates existing uses of a ∈ self_adjoint A to is_self_adjoint a so as to standardize. We also move several results into the is_self_adjoint namespace in order to take advantage of dot notation.