Let A=a11⋮ar1⋮as1⋮an1a12⋮ar2⋮as2⋮an2⋯⋱⋯⋱⋯⋱⋯a1n⋮arn⋮asn⋮ann be a square matrix of order n. Let \mapdetA denote the determinant of A. Let B=a11⋮ar1+kas1⋮as1⋮an1a12⋮ar2+kas2⋮as2⋮an2⋯⋱⋯⋱⋯⋱⋯a1n⋮arn+kasn⋮asn⋮ann. Then \mapdetB=\mapdetA. That is, the value of a determinant remains unchanged if a constant multiple of any row is added to any other row.
theorem Multiple_of_Row_Added_to_Row_of_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 sorry