Diagonal Matrix with Prescribed Diagonal

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\in\mathbb{N}$ and let $\lambda\in\mathbb{R}^{n}$, a point of $\mathbb{R}^{n}$ with components $\lambda_{i}$ as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, with real matrices, their entries, and the entries $\delta_{ij}$ of the identity matrix $I_{n}$.

¶ The diagonal matrix $\operatorname{diag}(\lambda)$ with diagonal $\lambda$ is the matrix $\operatorname{diag}(\lambda)\in\mathcal{M}_{n}(\mathbb{R})$ with entries

$$\operatorname{diag}(\lambda)_{ij}=\lambda_{i}\delta_{ij}\qquad(i,j\in[n]),$$

that is, the map $(i,j)\mapsto\lambda_{i}\delta_{ij}$ from $[n]\times[n]$ to $\mathbb{R}$, a map by Sets and Maps: Ordinary Notation §maps, and a real $n\times n$ matrix by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices.