mathlib3
feat(inner_product_space/positive): defines square root of a linear map
#18779
Open
Open