m : Type ?u.1700808
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ det (updateRow Aᵀ i fun k => A k i + c • A k j) = det Aᵀ
m : Type ?u.1700808
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ det (updateColumn A i fun k => A k i + c • A k j) = det A
rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
no goals
m : Type ?u.1700808
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ det (updateRow Aᵀ i fun k => A k i + c • A k j) = det Aᵀ
exact det_updateRow_add_smul_self Aᵀ hij c