The Positive Semidefinite Square Root of a Positive Semidefinite Matrix

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$ and let $A\in\mathcal{S}(n)$, the set of symmetric matrices, be positive semidefinite, with the matrix product.

¶ The positive semidefinite square root of $A$, written $A^{1/2}$, is the unique $B\in\mathcal{S}(n)$ that is positive semidefinite and satisfies $BB=A$, which exists and is unique by Every Positive Semidefinite Matrix Has Exactly One Positive Semidefinite Square Root §square-root.