basic): make starₗᵢ apply to normed star groups (#15173)

Commit

3 years ago

feat(analysis/normed_space/star/basic): make starₗᵢ apply to normed star groups (#15173)

Author

j-loreaux

Parents