by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
determinantlinear-algebramatrixproofwiki
Let a11⋮ar1⋮an1⋯⋱⋯⋱⋯a1s⋮ars⋮ans⋯⋱⋯⋱⋯a1n⋮arn⋮ann be a determinant. Then a11⋮ar1+ar1′⋮an1⋯⋱⋯⋱⋯a1s⋮ars+ars′⋮ans⋯⋱⋯⋱⋯a1n⋮arn+arn′⋮ann=a11⋮ar1⋮an1⋯⋱⋯⋱⋯a1s⋮ars⋮ans⋯⋱⋯⋱⋯a1n⋮arn⋮ann+a11⋮ar1′⋮an1⋯⋱⋯⋱⋯a1s⋮ars′⋮ans⋯⋱⋯⋱⋯a1n⋮arn′⋮ann. Similarly Then a11⋮ar1⋮an1⋯⋱⋯⋱⋯a1s+a1s′⋮ars+ars′⋮ans+ans′⋯⋱⋯⋱⋯a1n⋮arn⋮ann=a11⋮ar1⋮an1⋯⋱⋯⋱⋯a1s⋮ars⋮ans⋯⋱⋯⋱⋯a1n⋮arn⋮ann+a11⋮ar1⋮an1⋯⋱⋯⋱⋯a1s′⋮ars′⋮ans′⋯⋱⋯⋱⋯a1n⋮arn⋮ann.
theorem Determinant_as_Sum_of_Determinants {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (i : Fin n) (v w : Fin n → R) (h : A i = v + w) : A.det = (A.updateRow i v).det + (A.updateRow i w).det := by sorry