det_of_lowerTriangular — Mathlib

English

Similarly, for a lower-triangular matrix, the determinant is the product of its diagonal entries.

Русский

Аналогично, для нижнетреугольной матрицы детерминант равен произведению диагональных элементов.

LaTeX

$$$\det M = \prod_{i} M_{ii}$$$

Lean4

theorem det_of_lowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.BlockTriangular toDual) :
    M.det = ∏ i : m, M i i := by
  rw [← det_transpose]
  exact det_of_upperTriangular h.transpose

Похожие утверждения