Determinant_with_Row_Multiplied_by_Constant
Proveddeterminantlinear-algebramatrixproofwiki
Let be a square matrix of order . Let be the determinant of . Let be the matrix resulting from one row of having been multiplied by a constant . Then That is, multiplying one row of a square matrix by a constant multiplies its determinant by that constant.
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Determinant_with_Row_Multiplied_by_Constant {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (i : Fin n) (c : R) : (A.updateRow i (c • A i)).det = c * A.det := by sorrySource