m : Type ?u.1750254
n✝ : Type ?u.1750257
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i (Fin.succ j) = B i (Fin.succ j) + c j * A i (↑Fin.castSucc j)
⊢ det Aᵀ = det Bᵀ
m : Type ?u.1750254
n✝ : Type ?u.1750257
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i (Fin.succ j) = B i (Fin.succ j) + c j * A i (↑Fin.castSucc j)
⊢ det A = det B
rw [← det_transpose A, ← det_transpose B]
no goals
m : Type ?u.1750254
n✝ : Type ?u.1750257
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i (Fin.succ j) = B i (Fin.succ j) + c j * A i (↑Fin.castSucc j)
⊢ det Aᵀ = det Bᵀ
exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i