by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
determinantdiagonallinear-algebramatrixproofwiki
Let A=a110⋮00a22⋮0⋯⋯⋱⋯00⋮ann be a diagonal matrix. Then the determinant of A is the product of the elements of A. That is \ds\mapdetA=∏i=1naii