Lean-Workbook Plus 53656: Symmetric three-by-three determinant

For real $a,b,c$, the determinant of $\begin{pmatrix}-2a&a+b&c+a\\a+b&-2b&b+c\\c+a&b+c&-2c\end{pmatrix}$ is $4(a+b)(b+c)(c+a)$.

Source: Lean-Workbook row lean_workbook_plus_53656 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.