Effect_of_Elementary_Row_Operations_on_Determinant
Proveddeterminantelementary-operationslinear-algebramatrixproofwiki
Let be a square matrix of order . Let denote the determinant of . Take the elementary row operations {{axiom | n = \text {ERO} 1 | t = For some , multiply row by | m = r_i \to \lambda r_i }} {{axiom | n = \text {ERO} 2 | t = For some , add times row to row | m = r_i \to r_i + \lambda r_j }} {{axiom | n = \text {ERO} 3 | t = Exchange rows and | m = r_i \leftrightarrow r_j }} Applying has the effect of multiplying by . Applying has no effect on . Applying has the effect of multiplying by .
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Effect_of_Elementary_Row_Operations_on_Determinant {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (i j : Fin n) (hij : i ≠ j) (c : R) : (A.updateRow i (A i + c • A j)).det = A.det := by sorrySource