mathlib3

fec8ffec - chore(analysis/normed_space/star/*): migrate use of `a ∈ self_adjoint A` to `is_self_adjoint a` (#16212)

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.