lean_workbook_plus_53656
OpenProve that |\begin{ matrix } -2a & \quad \quad \quad \quad a+b & \quad \quad \quad \quad c+a \ a+b & \quad \quad -2b & \quad \quad \quad \quad b+c \ c+a & \quad \quad \quad \quad c+b & \quad \quad \quad \quad -2c \end{ matrix }|=\quad \quad 4(a+b)(b+c)(c+a)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53656 (a b c : ℝ) : Matrix.det (![![-2*a, a+b, c+a],![a+b, -2*b, b+c],![c+a, b+c, -2*c]]) = 4*(a+b)*(b+c)*(c+a) := by sorry
Source