Determinant_with_Unit_Element_in_Otherwise_Zero_Row

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

determinantlinear-algebramatrixproofwiki

Let $D$ be the determinant $D = \begin {vmatrix} 1 & 0 & \cdots & 0 \\ b_{2 1} & b_{2 2} & \cdots & b_{2 n} \\ \vdots & \vdots & \ddots & \vdots \\ b_{n 1} & b_{n 2} & \cdots & b_{n n} \end {vmatrix}$ Then $D = \begin {vmatrix} b_{2 2} & \cdots & b_{2 n} \\ \vdots & \ddots & \vdots \\ b_{n 2} & \cdots & b_{n n} \end {vmatrix}$

Preamble

import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Formal statement

theorem Determinant_with_Unit_Element_in_Otherwise_Zero_Row {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (h : ∀ j : Fin n.succ, j ≠ 0 → A 0 j = 0) (h1 : A 0 0 = 1) : A.det = (A.submatrix Fin.succ Fin.succ).det := by sorry

Source

https://proofwiki.org/wiki/Determinant_with_Unit_Element_in_Otherwise_Zero_Row

View graph